PSI's AI System Proves the Aaronson-Ambainis Quantum Conjecture in Lean

TL;DR

Physical Superintelligence, a physics lab structured as a public benefit corporation, announced on November 6 that a research system built in-house proved the Aaronson-Ambainis conjecture, open in quantum computing theory since 2008. The system ran instances of a non-public Anthropic model on PSI's own hardware, produced a complete proof on day three of the run, and improved it twice afterward. The paper and formalization are public: a Lean 4 development with 648 theorems and zero added axioms that two independent proof checkers accept. The Stanford group that proved the hardest special case in August calls it "a huge result."

The question that waited 18 years

Scott Aaronson and Andris Ambainis posed the conjecture in 2008, in a paper titled The Need for Structure in Quantum Speedups. The title is the argument. Shor's algorithm factors large numbers exponentially faster than any known classical method because factoring hides a repeating period a quantum computer can sample. Ask a yes-or-no question about a random bit string instead, with no promise attached, and nobody could prove the quantum machine keeps an exponential edge. A card sharp needs a stacked deck; the conjecture says random decks do not come stacked.

Formally, it is a statement about polynomials. Beals, Buhrman, Cleve, Mosca, and de Wolf showed in 1998 that a quantum algorithm making T queries induces a polynomial of degree at most 2T with values between 0 and 1. Aaronson and Ambainis conjectured that every such non-constant polynomial has an influential variable: one input bit whose flip, squared and averaged over all inputs, moves the value by at least a fixed power of variance over degree. Given that, a classical machine can imitate any T-query quantum algorithm on all but a small fraction of inputs, paying only a polynomial factor in queries.

PSI's proof delivers an explicit bound: some variable i satisfies Inf_i(f) >= (8*sqrt(15)/(125*pi^4)) * eps^(5/2) / d^6, which works out to at least (eps/d)^7, with the constant sitting around 0.0025. Nobody will put that bound on a poster, and it does not matter: the conjecture only asked for polynomial dependence on eps over d.

Three days, one harness, someone else's model

The announcement is spare on infrastructure and precise where it counts. The research system was developed internally, the run happened on PSI's infrastructure, and the model inside the loop was a non-public Anthropic model. A complete proof existed during the third day of the run; the system then worked on related open problems and improved the result twice, and Lean accepted the final version. Business Insider, which covered the announcement on November 7, reports that Anthropic did not respond when asked which model was used.

The repo's disclosure section is one paragraph and does the genre a favor: the mathematical statements, the first draft of the paper, and the Lean formalization were produced by AI models, inside a research harness David Turturean built at PSI. Turturean reviewed the paper and is responsible for its correctness. Jim Halverson audited the proof, and Phiala Shanahan commented on the Lean formalization.

How to make an extraordinary claim checkable

The formalization is the interesting engineering. The conjecture's statement lives in one file, Conjecture.lean, which imports only Mathlib and none of the project's own definitions. To confirm the repo proves the real conjecture rather than a lookalike, a reader checks one definition against the conjecture as printed in their paper and nothing else. Separating the statement from the proof is the whole trick, and most formalization projects fumble it.

Then the verification stack. A static audit confirms the sources contain no sorry, no axiom, no native_decide, and no custom elaborators. The axiom report on each final theorem lists exactly the three standard Lean principles Mathlib itself uses. Every declaration replays through the Lean kernel outside the elaborator, then through lean4lean, an independent implementation of the type checker, and comparator reruns the four final theorems with nanoda, a Rust checker, in a sandboxed GitHub-hosted run. Recorded counts: 84 modules, 761 declarations, 648 theorems, 113 definitions, zero axioms. Replaying everything costs 173 GB of memory in parallel, or 7.4 GB and 11 minutes with one thread.

Best detail in the repo: the control. It contains a small project in which a false statement is smuggled in with the kernel switched off. A normal build accepts it and the axiom report looks clean, and both replay checkers reject it. That is why the replays exist. The referee is a type checker, and it does not take vibes.

The README's trust-boundary section also lists what the checks do not cover: whether the Lean statement says what the English conjecture says (a human job, made small by the Mathlib-only statement file), the paper's prose, and the foundations themselves, meaning Lean's kernel and Mathlib. That paragraph is more honest than most research announcements manage.

What it settles, and who settled it

The consequence for quantum computing: on yes-or-no questions about random inputs, a quantum computer cannot save exponentially many queries over a classical one. Speedups at that scale need structure, like the period Shor exploits. In August, Guy Blanc, Jordan Docter, Carmen Strassle, and Li-Yang Tan of Stanford settled the parallel case, showing every fixed-round t-query quantum algorithm admits a classical simulation with t^(O(d^2)) queries; that paper appears at FOCS 2026. They have read PSI's proof, sent comments, and are writing a shorter exposition of it for experts. Their verdict, as quoted by PSI: "This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups."

The proof follows a 2023 plan by Shachar Lovett and Jiapeng Zhang that left one inequality open, and PSI's system replaced it with a new inequality proved by pairing up inputs using a determinant, extending David Reimer's Butterfly Lemma from his proof of the van den Berg-Kesten conjecture. The technique inventory reads like a garage sale of Boolean function analysis, assembled in a way nobody had assembled it before.

Then there is the identity of the prover. The model doing the mathematics belongs to Anthropic and is not public; the harness around it belongs to PSI, a public benefit corporation with a bit more than 25 researchers and engineers, $58 million raised led by Breakthrough Energy Ventures, and Matthew Pines as CEO. Business Insider sets the result in its season: OpenAI's September Navier-Stokes work, Terence Tao declaring math's "romantic era" over, and an MIT survey finding 76 percent of math grad students and postdocs now expect to leave academic research. Model access is becoming the commodity. Knowing which problem to point the model at, and how to check what comes back, is the part that still has a moat.

What to steal

• Put the statement in its own file with zero project imports. Anyone auditing whether you proved the real thing reads one definition, not your whole codebase.
• Replay, do not just build. A normal build accepted the repo's planted false theorem; the kernel replays rejected it. A verification that cannot fail a planted failure is decoration.
• Run a second, independent checker. Two implementations of the same type theory agreeing is worth more than any amount of confident prose.
• Publish counts and digests. 84 modules, 761 declarations, 648 theorems, 0 axioms, plus SHA-256 digests of exactly what was checked, makes the artifact auditable from the outside.
• Name the responsible human. "Produced by AI models, reviewed and owned by a person" is the disclosure template worth copying.

Caveats

• The run narrative (three days, two improvements, unreleased model) comes from PSI alone. Anthropic has not commented, and the model is not public, so that part is unverifiable.
• Lean verifies the formalized statement, not the English one. The Mathlib-only statement file makes checking the match a short job, but it remains a human job, and broad expert review began days ago.
• The Stanford endorsement is real but early; their exposition paper is not out.
• No peer review yet. The paper is a preprint in a repo, with the Lean development standing in for referees.
• This is query-complexity theory, not a claim about quantum hardware. Nothing here speeds up or slows down a cold QPU.

Key Takeaways

• On November 6, PSI announced a proof of the Aaronson-Ambainis conjecture, open since 2008, found by an in-house research system running a non-public Anthropic model on PSI infrastructure.
• The system had a complete proof on day three of the run and improved the result twice; Lean accepted the final version.
• The artifact is a Lean 4.33 formalization with 648 theorems across 84 modules and zero added axioms, re-checked by leanchecker, lean4lean, and nanoda via comparator, with a planted false theorem as a negative control.
• The theorem caps quantum speedups on random, unstructured inputs at polynomial; Stanford's August result covered fixed-round algorithms, and its authors call the full proof "a huge result" and are writing an exposition.
• The proof fills the gap in Lovett and Zhang's 2023 plan with a new determinant-pairing inequality that extends Reimer's Butterfly Lemma.
• PSI is a 25-person public benefit physics company with $58M raised; its contribution is the proving harness and the verification stack, and Anthropic has not commented on the model.

Sources: PSI, A proof of the Aaronson-Ambainis conjecture, PSI GitHub, paper and Lean formalization, Business Insider, Blanc, Docter, Strassle and Tan, Quantum Speedups Require Structure or Depth