NederlandsStart-up PSI uses AI to help publish five quantum proofs that a computer can check
Physical Superintelligence has used its own AI system to tackle five open questions in quantum information theory. Each proof is also written in Lean, a program that checks proofs step by step. Other researchers can now check them for themselves.
Physical Superintelligence (PSI), a young company raising money for a physics lab in which AI takes part from the start, published new results on 23 October on five open questions in quantum information theory. That field studies how information can be stored, sent and processed using the rules of the quantum world. It is the foundation of quantum computers and quantum communication.
The five questions come from the Open Quantum Problems, a list of unsolved problems in the field. The PSI researchers worked on them together with the company's own AI research system. According to the company, the AI helped, while the researchers guided and checked the work. For each result, the company describes how AI was used.
Proofs a computer can check
What makes this special is mainly the form. Each result comes not only with a scientific paper, but also with a version of the proof in Lean. Lean is a program that checks a mathematical proof step by step. It works a bit like a spell checker, but for logic: if a single step is wrong, Lean rejects the proof.
That matters especially with AI. AI models can write texts that sound convincing but still contain errors. A proof that Lean has approved does not have to be taken on trust. PSI therefore calls the publication an early test of the idea that AI can help with research that can really be checked, and not only with text that sounds believable.
Everything is public on GitHub: for each result the paper and the Lean files, with everything needed to run the check yourself. A separate script shows when the earlier versions of the papers were made.
What has been proved
The results are technical, but almost all of them are about entanglement. That is a special quantum link between particles: if you measure one particle, you immediately know something about the other, even when it is far away. Entanglement is the raw material of quantum communication.
- Not all entanglement is usable. For a certain kind of quantum state, the Werner states, PSI proves that within a certain range you can never extract from three copies the pure entangled pairs needed for quantum communication. Whether this also holds for more than three copies remains an open question.
- Connected, but no longer provable. In a simple model of empty vacuum, two regions of space stay entangled however far apart they are. Yet PSI proves that beyond a certain distance, the well-known CHSH test can no longer show that their connection is stronger than ordinary physics allows.
- The best way to measure. For another test, the CGLMP test, PSI shows which way of measuring gives the strongest quantum effect, and that every best way essentially comes down to that one.
- Breaking entanglement. A recent paper by OpenAI reported that two operations of a certain kind (PPT maps) are in general not enough to break entanglement completely. PSI proves how many are always enough: 2(d−1), where d stands for the size of the quantum system.
- A counterexample. Finally, PSI found a counterexample to a conjecture about causal processes. Not every process in which cause and effect stay neatly in order fits into a larger, reversible quantum process of finite size.
Now it is up to other researchers
These are preprints. They do not yet have a DOI or arXiv number, the fixed identifiers of a scientific publication, and have not yet been reviewed by other researchers. The theorems are therefore claims by PSI itself. Thanks to the Lean proofs, other researchers can now check them for themselves: that is the next step.
PSI also has plans for data centres. According to the company, these are separate from this research.
What does this mean for the road to the singularity?
AI that helps with new mathematical proofs is a step towards AI that speeds up science. The biggest problem here is that AI can make mistakes that sound convincing. If proofs are routinely checked by a program like Lean, researchers can build on each other's work faster and with more confidence, even when part of it was done by AI. These five results are an early trial. Once other researchers have checked the proofs, it will become clear how well this way of working performs and whether it also fits other fields. And quantum information theory is itself a building block for the quantum computers of the future.
What is the technological singularity? Read the explanation →
