AI system using unreleased Anthropic model proves Aaronson-Ambainis conjecture, Lean-verified

Physical Superintelligence (PSI), an AI-native physics lab, announced on November 6, 2026 that an internal research system has proved the Aaronson-Ambainis conjecture, a question in quantum complexity theory that had been open since 2008. The system ran instances of an Anthropic model that has not been released to the public, and according to the announcement as reported on dev.to, the Lean proof assistant accepted the argument. The manuscript and the Lean 4 formalization have been made public; the paper has not been peer reviewed.

What the conjecture says

Scott Aaronson and Andris Ambainis posed the conjecture in 2008 to address a basic question: when can quantum computers be exponentially faster than ordinary ones? Dramatic speedups, such as Peter Shor's 1994 factoring algorithm, depend on structure — a promise that the input hides a specific pattern. Whether quantum machines could win exponentially on random inputs, which almost never carry such structure, was unknown. Aaronson and Ambainis reframed the question as a statement about polynomials and showed that, if it held, quantum computers would be at most polynomially faster than classical ones on random inputs.

How the system found the proof

PSI says a complete proof arrived during the third day of a run on the company's own infrastructure. The system was then directed at related open problems, improved the result twice, and Lean accepted the final version. The argument follows a plan set out by Shachar Lovett and Jiapeng Zhang, who had reduced the problem to a single inequality they left as a conjecture. PSI's proof substitutes a new inequality, proved in the manuscript through a pairing construction that builds on David Reimer's Butterfly Lemma.

David Turturean, a member of PSI's technical staff, led the work: he developed the research system, scoped the problem, prompted the model to assemble a first draft, reviewed it, and is named as responsible for the paper's correctness. Jim Halverson, a PSI adviser, audited the proof, and fellow adviser Phiala Shanahan commented on the Lean formalization. PSI states that the mathematical statements, the paper's first draft and the Lean formalization were all produced by AI models.

What the result establishes

The headline bound is concrete: if a polynomial varies by an amount v and has degree d, then some single input bit has influence at least c·v^(5/2)/d^6, where c is roughly 0.0025 — in other words at least (v/d)^7. In practical terms, an ordinary computer can now predict a quantum computer's probability of answering yes, up to small error, for all but a small fraction of random inputs, using a number of input reads that grows at most polynomially with the quantum machine's. On yes-or-no questions about random data, exponential quantum savings are impossible unless the input conceals a rare pattern. This is a result about limits, not engineering: it says nothing against structured problems such as factoring, where quantum speedups remain.

Verification and remaining caveats

The verification has explicit boundaries. The proof has not been peer reviewed, the human-readable paper is not itself machine-checked, and readers still need to confirm that the formal statement Lean verified matches the printed conjecture. The dev.to report, citing Unite.AI, adds that the formal development contains no proof placeholders or added axioms, and that its declarations were replayed through Lean's kernel and through lean4lean, an independent implementation of Lean's type checker.

A Stanford group — Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — settled a special case of the conjecture's prediction in August 2026 and has been reading the full proof, calling it "a huge result" and preparing a shorter exposition for specialists.

Why it matters

The result carries two stories at once. For quantum computing, it closes one of the field's central open problems and draws a clean boundary: exponential advantage requires structure in the input. For AI, it is a machine-checked proof of a problem that resisted human mathematicians for 18 years, produced by a model the public cannot use — a marker of how far internal research systems have moved past publicly available ones. The dev.to report also notes METR's November estimate that Anthropic's capabilities are improving at roughly twice the rate of an earlier period, with AI itself driving much of that acceleration.

What remains open is human work: whether the formal statement matches the original conjecture, and with it whether November 6, 2026 becomes the day a conjecture turned into a theorem or the day a machine-checked argument still needed people to say exactly what it proved.