Physical Superintelligence publishes Lean-checked proof of the Aaronson-Ambainis conjecture

What PSI announced

Physical Superintelligence, a research company also known as PSI, said on 6 November 2026 that it had proved the Aaronson-Ambainis conjecture and published a paper and Lean 4 formalization on GitHub. The paper is credited to David Turturean of PSI. Its AI disclosure says the mathematical statements, the first draft and the formalization were produced by AI models, run in a research harness Turturean built and ran on PSI's infrastructure.

The models were instances of what the paper calls "a non-public Anthropic model". They searched for existing ideas, proposed and tested new ones, and supervised each other. Turturean says he reviewed and edited the draft and is responsible for its correctness. Anthropic has not named the model.

The timeline appendix says the first complete proof was written on the third day of the run and checked in Lean, with a weaker exponent of 22. Asked to push further, the models improved it to 11 and then to 7, each version again checked in Lean.

What the conjecture says

Scott Aaronson and Andris Ambainis conjectured that every bounded, low-degree polynomial on the discrete cube has an influential variable: one input whose flipping changes the output noticeably. The conjecture appears in their paper "The need for structure in quantum speedups" (Theory of Computing, 2014) and had been open since around 2008.

It matters because the acceptance probability of a quantum algorithm making T queries is such a polynomial. If the conjecture holds, a classical algorithm can approximate any such quantum algorithm on most inputs with a polynomial number of queries. The paper proves the bound with influence at least a constant times Var(f)^(5/2)/d^6, or (ε/d)^7 in the original form. Its abstract says this confirms that superpolynomial quantum speedups in the query model need structure, such as a promise on the inputs.

The proof follows a plan by Shachar Lovett and Jiapeng Zhang and closes the inequality their plan left as a conjecture. It also builds on work by David Reimer, by Jeff Kahn, Michael Saks and Clifford Smyth, and by Avantika Agarwal and Shalev Ben-David.

How it was checked

The repository says the four public theorems contain no sorry placeholder and no added axiom, and depend only on Lean's three standard axioms. Every declaration was replayed through the Lean kernel and through lean4lean, an independent type checker. The Comparator tool accepted the theorems against a challenge file that imports only the statement. The Lean sources run to about 9,600 lines.

The authors list what the checks do not cover: whether the formal statement matches the printed conjecture, which a reader must confirm, and the paper itself. The acknowledgements thank Jim Halverson for auditing the proof and Phiala Shanahan for comments on the formalization. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan are writing a shorter exposition for experts.

Aaronson wrote on his blog that he believes the proof is correct, citing the Lean certificate and expert review, though he had not yet worked through it himself.

What it means and what to watch

This is a clearer case than most AI mathematics claims: a named open problem, a public formal proof and a positive early reading from the conjecture's author. It follows Axiom Math's Lean formalization of the finite simple groups classification and Google DeepMind's RSA work. Aaronson stressed that the result rules out only a type of quantum speedup researchers already expected not to exist. Watch for peer review, the Stanford exposition and whether Anthropic names the model. More in AI research.

For AI labs the result is also a product signal. The work ran on a model the public cannot use, so outsiders cannot repeat the run, only check its output. That is the trade the Lean file makes possible: the process stays private while the result can be verified by anyone with a laptop and the pinned toolchain. PSI says the result does not change post-quantum cryptography timelines, since the theorem concerns inputs without structure.

Questions people ask

What is the Aaronson-Ambainis conjecture?

A claim that every bounded low-degree polynomial on the discrete cube has an influential variable. It implies classical algorithms can approximate quantum query algorithms on most inputs.

Which AI model proved it?

PSI's paper says instances of a non-public Anthropic model, run inside a harness built by David Turturean. The model has not been named.

Has the proof been verified?

Lean's kernel and an independent checker accepted the formal proof. Whether the formal statement matches the conjecture, and the paper, still need human review.

Sources

1. A proof of the Aaronson-Ambainis conjecture (paper and Lean 4 formalization) (Physical Superintelligence, 6 Nov 2026)
2. A proof of the Aaronson-Ambainis conjecture (Physical Superintelligence, 6 Nov 2026)
3. Aaronson-Ambainis Conjecture proved! (By AI, of course) (Shtetl-Optimized, 7 Nov 2026)
4. AI-Assisted Proof Settles Longstanding Question About Quantum Speedups (The Quantum Insider, 6 Nov 2026)