PSI: AI found proof of a 2008 conjecture on the limits of quantum computers
The US company Physical Superintelligence says its AI system found a proof of the Aaronson-Ambainis conjecture, an open question from 2008 about when quantum computers are much faster. The program Lean has approved the proof; fellow researchers are now checking it.
At the end of October we wrote about five proofs in quantum information theory that the US company Physical Superintelligence (PSI) found with the help of its own AI system. Each of those proofs was also checked by Lean, a program that goes through a mathematical proof step by step. Now PSI reports a much bigger result: according to the company, its AI system has found a proof of the Aaronson-Ambainis conjecture, an open question from 2008 about the limits of quantum computers. PSI announced this on 6 November.
A conjecture is a mathematical statement that many researchers believe to be true, but that nobody has proven yet. This conjecture is named after the computer scientists Scott Aaronson (University of Texas at Austin) and Andris Ambainis, and is seen as one of the central open questions about quantum computers. PSI is a young company from Cambridge in the US state of Massachusetts. It started in September 2026 and wants to be a physics lab built on AI from the beginning.
Why this question matters
Quantum computers can solve some problems much faster than ordinary computers. The best-known example is the algorithm of the mathematician Peter Shor from 1994, which breaks large numbers down into the prime numbers they are made of. In all known examples of such a huge gain, the problem has a special regularity. In Shor's case it is a pattern in the numbers that keeps repeating. Aaronson and Ambainis asked whether this is always so. Can a quantum computer also be enormously faster with ordinary, random input, without such a regularity?
To measure this, researchers count how often an algorithm has to look at the input. Suppose the input is a long row of zeros and ones, and the algorithm has to answer a yes-or-no question about that row. Each time it looks at one place in the row, that counts as one step. The question is then how many steps an ordinary computer needs to do the same as a quantum computer.
What matters is how the difference grows. With an exponential difference, the number of steps of the ordinary computer doubles, for example, with every extra step of the quantum computer: for 10 quantum steps it is well over a thousand, for 20 already over a million. With a polynomial difference, it grows much more slowly, like a square or another fixed power: 100 for 10 quantum steps, 400 for 20 steps.
Aaronson and Ambainis showed that their conjecture, if it is correct, gives the answer. Then an ordinary computer can predict the answer of a quantum computer for almost all input, using a number of steps that is at most polynomially larger. Big quantum gains then always require input with a special structure.
What the conjecture says
The conjecture itself is about formulas. The probability that a quantum algorithm answers "yes" can be written as a formula containing the zeros and ones of the input, a so-called polynomial. Researchers had already proven in the late 1990s that this formula is simpler the fewer steps the algorithm takes.
The conjecture says: as long as the result of such a formula is not the same for every input, there is always at least one place in the input with a noticeable influence. By influence, mathematicians mean how much the result changes on average if you change a zero into a one at that one place, or the other way round.
That helps an ordinary computer. If there is always such an influential place, it can look at that place first. That fixes part of the result. According to the conjecture, what is still uncertain again contains an influential place, which it looks at next. In this way the result becomes more certain with every step, until it is almost fixed for nearly all input. Then the ordinary computer knows what the quantum computer would answer.
The difficult part was how large that influence is at least. As early as 2006, other researchers proved that such a place always exists. But the influence they could guarantee became exponentially smaller as the formula became more complicated. With such a small influence, each step of the ordinary computer changes the uncertainty so little that it needs an enormous number of steps, and little is left of the approach. PSI now says it has proven that the influence only becomes polynomially smaller, so much more slowly. That is exactly what Aaronson and Ambainis suspected.
How the proof was found
PSI used a research system that it built itself and that worked with a non-public AI model from the AI company Anthropic. The company does not name that model. According to PSI, on the third day of a computing session on its own computers, the system had a complete proof, and Lean approved it. PSI then let the system tackle related open questions. In doing so, the system improved the result twice more, and Lean approved that final version too.
According to PSI, the AI produced the mathematical statements, the first version of the paper and the version of the proof in Lean. David Turturean, a researcher at PSI, built the system, chose the problem, ran the system and has proofread the paper. He is responsible for its correctness. Jim Halverson, an adviser to PSI, checked the proof, and adviser Phiala Shanahan commented on the Lean version.
The proof follows a plan by the mathematicians Shachar Lovett and Jiapeng Zhang. They had mapped out a route to the proof, but one intermediate step in it had not yet been proven. The new proof replaces that intermediate step with another one, which PSI did prove.
That Lean checks the proof is especially valuable here. At the end of 2019, two mathematicians already reported a proof of the same conjecture, but it turned out to contain a subtle error. Lean only approves a proof if every step is correct. What people still need to check is whether the statement as written in Lean says exactly the same as the conjecture on paper. PSI has put those statements in one separate file, which fellow researchers can read through. The paper, the Lean proof and the software to run the check are publicly available on GitHub.
Fellow researchers are reading along
In August 2026, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford University proved part of the conjecture. They showed that for random input there is no exponential gain for quantum algorithms that look at the input in a fixed number of rounds, with many places at once in each round. They are now reading PSI's proof, have already sent comments and are writing a shorter explanation for fellow researchers. On PSI's website they call it an enormous result that settles a decades-old conjecture.
The paper has not yet appeared in a scientific journal and has not yet been formally reviewed by other researchers. By the evening of 6 November, Aaronson and Ambainis had not yet responded publicly. Now it is up to more researchers to go through the proof. Because everything is public, they can start right away.
What does this mean for the road to the singularity?
Experts worked on this conjecture for eighteen years, and an earlier proof turned out to be wrong. Now, according to PSI, an AI system found within a few days a proof that a computer has checked step by step. If the proof holds up with fellow researchers, it is a clear example of AI solving a well-known open question in mathematics, with people choosing the problem and checking the result.
The result itself also says something about quantum computers. If the proof is correct, it is established that anyone looking for a big quantum gain has to look at problems with a special structure, as with Shor. That helps researchers search in a more targeted way for tasks where quantum computers really make the difference. And because a computer can check any proof of this kind, researchers do not have to take an AI's work on trust. That makes it easier to build on it.
What is the technological singularity? Read the explanation →
Sources
- OfficeChai
- psi.inc
- GitHub: physical-superintelligence/aaronson-ambainis (paper en Lean-bewijs)
- RuntimeWire
- Aaronson en Ambainis, The need for structure in quantum speedups
- Bhattacharya, Aaronson-Ambainis Conjecture Is True For Random Restrictions (arXiv)
- Quantum Speedups Require Structure or Depth (arXiv)
In the glossary: Logical qubit, Quantum computer, Quantum error correction, Qubit, Lean