AI System Claims Lean-Checked Proof of the Aaronson-Ambainis Conjecture
On 6 November 2026, Physical Superintelligence (PSI) said an internal research system running a non-public Anthropic model produced a proof of the Aaronson-Ambainis conjecture, a long-open problem about when quantum computers can beat classical ones on random inputs. The proof is formalized in Lean 4 and public on GitHub, but it is a preprint without peer review or independent expert confirmation yet.
On this page
What PSI announced
Physical Superintelligence, a research company, said on 6 November that an AI research system it built internally, running a non-public Anthropic model, produced a complete proof of the Aaronson-Ambainis conjecture. According to PSI, the system had a full proof during the third day of its run, the Lean proof assistant accepted it, and the system then improved the result twice more, with Lean accepting the final version.
The work is public. A GitHub repository holds the Lean 4 formalization, built against Mathlib, alongside a paper draft that the repository describes as a preprint. PSI credits David Turturean with building the research harness, scoping the problem, and taking responsibility for the paper's correctness, while advisers Jim Halverson and Phiala Shanahan audited the proof and commented on the formalization. PSI has not named the Anthropic model it used.
Why this conjecture matters
Scott Aaronson and Andris Ambainis posed the conjecture in their 2014 paper on the need for structure in quantum speedups. The question is when a quantum computer can be exponentially faster than an ordinary one. Famous speedups such as Shor's factoring algorithm rely on structure in the problem, like a promised repeating pattern. The conjecture says that without such structure, on yes-or-no questions about random inputs, a quantum computer is at most polynomially faster.
In mathematical terms, it says any bounded low-degree polynomial with enough variance must have at least one input variable with noticeable influence. PSI's version gives an explicit bound, which its repository states with a constant of about 0.0025. The PSI web page prints that constant in a form that appears garbled, so the GitHub statement is the one to read.
Before this, the strongest progress was a special case. In August, Guy Blanc, Jordan Docter, Carmen Strassle, and Li-Yang Tan showed that quantum algorithms with a fixed number of parallel rounds can be simulated classically on most inputs, a result accepted at FOCS 2026. PSI quotes that group calling the new proof "a huge result" and says they are writing a shorter exposition.
How much the Lean check proves
The repository says the Lean development is complete, with no placeholder proofs and no added axioms, and that the final theorems rely only on Lean's three standard axioms. The authors report replaying the proof with Lean's kernel checker and a second independent checker, lean4lean. Three of the four headline theorems carry no extra assumptions; a fourth, sharper bound depends on a published result that is not itself formalized.
A machine check is strong evidence that the formal statement is proved, but it does not certify that the formal statement matches the conjecture as mathematicians intend it. The repository says so directly: readers must confirm the Lean statement matches the original, and the written paper is not machine-checked.
What is still unconfirmed
The claim is about a day old and rests on PSI's own page and repository. No peer review has been reported, and as of 7 November Scott Aaronson's blog had not commented. PSI also has not disclosed how much compute the three-day run used.
Even so, this fits a pattern this year of AI systems pairing with proof assistants on real mathematics. The Lean files are open, so anyone with a capable machine can replay the check on their own hardware; the repository says a serial replay takes about 11 minutes and 7.4 GB of memory. That kind of local, checkable evidence is what will settle whether the result holds.