On November 6, Physical Superintelligence (PSI) published a proof of the Aaronson-Ambainis conjecture. According to the company, it was found by an internally built research system running instances of an unreleased Anthropic model on PSI’s own infrastructure. The conjecture has been open since 2008 and counts as one of the central problems in quantum complexity theory.
The question behind it is old and practical at once: when are quantum computers genuinely exponentially faster? Shor’s 1994 factoring algorithm is, because its input hides a repeating pattern the algorithm can exploit. Whether that advantage survives on random inputs, where such patterns almost never exist, nobody knew.
What has now been proved
Scott Aaronson and Andris Ambainis translated the question into pure mathematics. Their conjecture says every bounded low-degree polynomial has at least one variable with large influence. From it follows this: on yes-or-no questions over random inputs, an ordinary computer can estimate a quantum algorithm’s probability of answering yes using polynomially rather than exponentially many looks at the data.
Only those looks are counted, not total running time. For problems with suitable structure, an exponential quantum advantage therefore remains possible. What falls is the hope of an advantage without structure.
The proof follows a plan by Shachar Lovett and Jiapeng Zhang but replaces an inequality they had left conjectural with a new all-pairs inequality, and sharpens David Reimer’s Butterfly Lemma to get there.
Who checked what
That is the more interesting part. PSI says the system had a complete proof on day three of the run and that Lean accepted it. The system was then set loose on related open problems and improved the result twice, until Lean accepted the final version.
Per the audit recorded in the repository, the formal development contains no proof placeholders and no added axioms. The declarations were replayed through Lean’s kernel and through lean4lean, an independent implementation of the type checker. In a sandboxed run, a comparator built from the nanoda and Lean kernels accepted the four final theorems, and on a second machine it rejected four deliberately wrong ones.
The limits sit right next to that. A human still has to confirm that the formal statement matches the printed conjecture. The readable paper itself is not machine-checked. Lean’s kernel, Lean’s compiler, Mathlib’s definitions and the machines used for checking all remain part of the trusted base.
David Turturean, on PSI’s technical staff, built the system, scoped the problem, reviewed the first draft, and takes responsibility for its correctness. The mathematical statements, the draft and the Lean formalization were produced by AI models, according to the repository. Jim Halverson audited; Phiala Shanahan commented on the formalization.
The verdict comes from the people working next door
In August 2026, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan at Stanford settled a special case: no exponential savings on random inputs for quantum algorithms restricted to a fixed number of parallel rounds. That same group has been reading the new proof, has sent comments, and is writing a shorter exposition for experts. Their verdict, quoted by PSI: “This is a huge result.”
That is the confirmation that counts, and so far it appears only in PSI’s own post. Until an independent publication follows, this is a very well-documented claim rather than a textbook theorem. It stays remarkable either way: the model that found the proof is one nobody outside can touch.