An artificial intelligence system has produced a proof of one of quantum computing’s longest-standing open problems, according to the lab behind the work — a claim that, if it survives expert scrutiny, would settle a question mathematicians have chased since 2008.
Physical Superintelligence (PSI) said on 6 November that a research system it developed internally, running instances of a model from Anthropic that has not been publicly released, found a complete proof of the Aaronson-Ambainis conjecture during the third day of a run on the lab’s own infrastructure. The proof was then checked step by step by Lean, a proof assistant in which a computer verifies every line of an argument, and Lean accepted it. PSI says the system went on to improve the result twice, with Lean accepting the final version.
The conjecture, posed by Scott Aaronson and Andris Ambainis, asks when quantum computers can be exponentially faster than ordinary ones. The most famous quantum speedups, such as Peter Shor’s 1994 algorithm for factoring large numbers, work because the problem hides a repeating pattern that the quantum computer can exploit. What was unknown was whether a quantum computer could enjoy a similar exponential advantage on random, unstructured inputs, where no such pattern exists.
Aaronson and Ambainis reduced that question to pure mathematics: a statement about polynomials, showing that if it held, a quantum computer could be at most polynomially faster than a classical one on random inputs. PSI’s proof follows a plan set out by Shachar Lovett and Jiapeng Zhang, replacing one inequality their plan had left conjectural with a new one proved using a pairing of input settings generated by a determinant. The lab has published both the manuscript and the full Lean formalisation, so independent researchers can replay the machine-checked argument for themselves.
The result is not yet peer-reviewed, and PSI is open about its limits. The Lean check confirms the formal argument is internally consistent, but human mathematicians must still confirm that the formal statement in the code matches the conjecture as Aaronson and Ambainis meant it, and the human-readable paper itself is not machine-checked. Researchers at Stanford University who settled a special case of the conjecture in August have been reading the full proof and are preparing a shorter exposition for experts; they described it as “a huge result” that “resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups”.
If the proof holds up, it draws a firm line around quantum advantage: exponential speedups need structure in the problem. On random, unstructured data, a quantum computer’s edge over an ordinary one is, at most, modest.
Note: This story is single-sourced from PSI’s own announcement and has not been independently verified by peer review. The claim rests on PSI’s published proof and Lean formalisation, which experts are now examining.
Sources: Physical Superintelligence, “A proof of the Aaronson-Ambainis conjecture”, https://psi.inc/research/aaronson-ambainis/ ; Unite.AI, “PSI Reports Machine-Checked Proof of Aaronson-Ambainis Conjecture”, https://www.unite.ai/psi-reports-machine-checked-proof-of-aaronson-ambainis-conjecture/
