Physical Superintelligence (PSI) announced on 6 November 2026 that an internal AI research system running instances of a non-public Anthropic model found a proof of the Aaronson-Ambainis conjecture, a quantum-computing question open since 2008. The system produced a complete proof during the third day of a run on PSI's own infrastructure, and Lean — a proof assistant that machine-checks every step of a mathematical argument — accepted it. PSI then set the system on related open problems, improved the result twice, and Lean accepted the final version. The manuscript and the Lean 4 formalization are public.

The conjecture asks when quantum computers can be exponentially faster than classical machines. If PSI's proof holds, an ordinary computer can estimate a quantum algorithm's probability of answering yes, on most inputs and within a fixed margin of error, without exponentially more reads of the input — in other words, exponential quantum speedups require special patterns or structure in the problem, a limit that was long suspected but never proved. PSI says its proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang, who had left one key inequality unproved; the new paper proves a replacement inequality and gives an explicit bound.

What makes the claim harder to dismiss than a typical "AI solved math" headline is the checking. PSI's repository says the formal development contains no proof placeholders or added axioms, and its declarations were replayed through Lean's kernel and lean4lean, an independent implementation of Lean's type checker. In a sandboxed run, a comparator using the nanoda and Lean kernels accepted the four final theorems, and on a second machine it accepted one correct small solution and rejected four deliberately wrong ones. David Turturean, a member of PSI's technical staff, built the research system, scoped the problem, prompted the model to package a first draft, reviewed that draft and is responsible for the paper's correctness; PSI adviser Jim Halverson audited the proof, and the repository discloses that AI models produced the mathematical statements, first draft and Lean formalization.

The caveats are real and PSI states them itself. The result is not peer-reviewed: the proof has not yet passed journal review, and human experts still have to confirm that the formal statement encoded in Lean matches the conjecture as Aaronson and Ambainis meant it — the human-readable paper is not itself machine-checked. Four Stanford researchers who settled a special case in August 2026 are reading the proof and writing a shorter version for experts. Treat this as a company claim with a checkable artifact, not a journal verdict — but it is a striking one: it follows OpenAI's release of 722 AI-written math manuscripts in October, and it is the strongest evidence yet that AI systems are moving from assisting proofs to producing them.

Sources