Aaronson-Ambainis Conjecture: An AI Proved an 18-Year-Old Quantum Puzzle in Three Days

On November 6, a small company called Physical Superintelligence (PSI) announced something that would have sounded like science fiction a decade ago: an AI research system, running a non-public Anthropic model, had proved the Aaronson-Ambainis conjecture, a central open problem in quantum complexity theory that had stood since 2008. The system had a complete proof by the third day of the run. Lean, the proof assistant that checks every logical step by machine, accepted it. PSI then set the system loose on related problems, improved the result twice, and published both a paper and the public Lean formalization so anyone can re-check the work.

To see why this matters, start with what quantum computers are actually good at. In 1994, Peter Shor found a quantum algorithm that factors large numbers far faster than any known classical method. But Shor's speedup leans on a rare gift: the problem hides a repeating pattern, and the quantum computer finds how often it repeats. Most dramatic quantum speedups known work the same way. They exploit structure.

Scott Aaronson and Andris Ambainis asked the uncomfortable question: what about random inputs, which almost never have that structure? Can a quantum computer answer a yes-or-no question about a random string with exponentially fewer looks at the bits than an ordinary computer? They stated a conjecture about polynomials — pure mathematics — and showed that if it is true, the answer is no: on random inputs, quantum computers are at most polynomially faster. The conjecture became one of the central open problems of quantum complexity theory, and in August 2026 a Stanford group proved it for a special case: quantum algorithms that read their input in a fixed number of parallel rounds.

PSI's proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang, replacing one inequality their plan left as a conjecture with a new inequality proved in the manuscript, using a pairing argument built on David Reimer's Butterfly Lemma and results from several other groups. The human in the loop, PSI's David Turturean, built the research system, scoped the problem, ran it, and takes responsibility for the paper's correctness. Advisor Jim Halverson audited the proof. The Stanford group that proved the special case has been reading the full proof, sent comments, and is writing a shorter exposition for experts. Their verdict so far: "This is a huge result."

That is the right way to read this story — not as a coronation, but as a claim with a checkable artifact. Lean acceptance is a high bar: a machine has verified every step of the argument. What Lean cannot check is whether the formal statement is the statement mathematicians actually care about, or whether the formalization smuggles in a hidden assumption. That is the job of human experts, and it is still pending. Peer review has not happened. The model that found the proof is not public, so nobody can re-run the discovery itself — only inspect what it produced.

And that is where the week this announcement landed in becomes the real story. PSI's proof is not an isolated event. In October, OpenAI released 722 AI-written mathematics manuscripts, including claimed proofs of the quasi-Riemann hypothesis, the Unique Games Conjecture, and the Hodge conjecture for a special class of shapes. In September, a paper in The Quarterly Journal of Mathematics reported an AI system finding the key idea that turned conditional results about k-differentials into unconditional theorems, with the crucial lemma formally proved in Lean. Axiom has formalized the roughly 7,500-page Stacks Project — some 16 million lines — making a huge body of algebraic geometry machine-checkable. The pattern is now unmistakable: AI proposes, and Lean disposes. The bottleneck has moved from finding proofs to verifying them, and verification is where humans still set the pace.

That shift is what I am watching. If the Stanford exposition lands cleanly and no rival group finds a gap, the Aaronson-Ambainis proof becomes the second major AI-claimed result in a month to survive expert scrutiny — and the question stops being whether AI can do frontier mathematics and becomes how fast the verification pipeline can keep up. My prediction: by 31 December 2027, this proof will have been publicly confirmed by independent mathematicians, through the Stanford group's exposition, a peer-reviewed publication, or an equivalent public expert confirmation, with no material gap found. I put that at 65% — the mechanical bar is already cleared, the right experts are already engaged, but human confirmation is not a formality, and a single definitional mismatch can still sink a Lean-checked proof.