PSI: Lean Proof of Aaronson-Ambainis Conjecture Found by AI System
Physical Superintelligence announced that an internal search system, powered by an unreleased Anthropic model, found a proof of the Aaronson-Ambainis conjecture (2008) that was accepted by Lean 4. Both the manuscript and the formalization have been made public.
Physical Superintelligence (PSI) announced on November 6, 2026, that an internal search system, powered by instances of an unreleased Anthropic model, discovered a proof of the Aaronson-Ambainis conjecture, open since 2008. According to the lab, Lean accepted a complete proof on the third day of the run, followed by two subsequent refinements. Both the manuscript and the Lean 4 formalization are public.
What the Conjecture States
Scott Aaronson and Andris Ambainis investigated whether a quantum computer could answer a yes/no question about a random string with exponentially fewer queries than a classical computer. Most known dramatic speedups (such as Shor’s algorithm) rely on rare structure within the input. Their pure mathematics conjecture, if true, implies that in the absence of such structure, the classical overhead remains at most polynomial in the number of quantum queries.
Specifically, after T queries, the probability that a quantum algorithm outputs “yes” is a polynomial of degree at most 2T taking values in [0, 1]. The conjecture asserts that any such polynomial, provided it varies sufficiently, always possesses a variable with high enough influence—allowing a classical computer to mimic the prediction by inspecting only a small number of bits.
What PSI Released
The research page and GitHub repository describe a proof following a blueprint by Lovett and Zhang, resolving an inequality that had been left open. The README claims four Lean theorems without placeholders or added axioms, re-checked by two implementations of the Lean kernel (toolchain 4.33.0 / Mathlib v4.33.0, Apache 2.0 license). David Turturean led the effort; Jim Halverson audited the proof; Phiala Shanahan commented on the formalization.
In August 2026, four Stanford researchers (Blanc, Docter, Strassle, and Tan) had already settled a special case. PSI notes that they are currently reviewing the full proof and preparing an exposition with a shorter write-up; the lab quotes a complimentary comment from them.
Caveats to Keep in Mind
The repository leaves it to the reader to verify that the Lean statement PrintedConjecture faithfully captures the printed conjecture. An improved theorem relies on an assumption by Agarwal and Ben-David that is not formalized here. The prose paper itself is not machine-checked. The Anthropic model is neither named nor public: the output can be inspected, but the discovery process cannot be rerun. No public reaction from Aaronson or Ambainis was found at the time of writing.
Our take
The takeaway here is not that “a model invented number theory,” but that a search system paired with a formal verifier can now produce an inspectable artifact on an eighteen-year-old open problem. The machine proposes, Lean handles part of the verification, and humans remain responsible for ensuring the formalized statement aligns with the original conjecture. Until that fidelity and peer review are fully resolved, the best approach is to treat the repository as a machine-verified candidate proof, rather than a theorem already etched into the mathematical canon.
Sources
- PSI — A proof of the Aaronson-Ambainis conjecture (November 6, 2026) Primary source
- GitHub — physical-superintelligence/aaronson-ambainis (paper + Lean 4) Primary source
- Aaronson & Ambainis — The Need for Structure in Quantum Speedups (arXiv:0911.0996) Primary source — Original statement of the conjecture
A primary source comes directly from the company, lab or organization concerned. A secondary source reports the information without being its author: we flag it as such. Spotted an error? See our corrections policy.
