PSI Claims AI-Assisted Lean Proof of the Aaronson–Ambainis Conjecture
Physical Superintelligence says an internal system using a non-public Anthropic model produced a Lean-accepted proof of the 2008 quantum-query conjecture; a public repo is checkable, but key caveats remain.
Published
Last updated / Fact-checked on
Illustrative photo of someone working on a laptop with notes — not PSI staff, not a Lean session, and not evidence of the claimed proof. Photo by StartupStockPhotos on Pixabay — Pixabay Content License
Physical Superintelligence (PSI) published a research page on November 6, 2026, stating that the Aaronson–Ambainis conjecture “is now a theorem.” According to PSI, an internal research system using instances of a non-public Anthropic model on PSI’s infrastructure found a complete proof by the third day of a run; Lean accepted that proof. PSI says the system later improved the result twice, and Lean accepted the final version. The company frames the implication as: for yes/no questions on random strings, a quantum computer cannot save exponentially many input reads unless the string has rare structure. That framing is PSI’s; outside peer review and mathematician endorsement are not in the sources used here.
At a glance
| Aspect | What PSI claims | What is publicly checkable / caveated |
|---|---|---|
| Process | Non-public Anthropic model in PSI system; proof by day three; two later improvements; Lean accepted | Public repo physical-superintelligence/aaronson-ambainis with paper + Lean 4 formalization |
| Formal proofs | Lean accepted the proofs | README: four final theorems, no placeholders/added axioms; describes kernel replay, lean4lean, comparator (we did not re-run these) |
| Statement match | Presents result as the conjecture | README: whether PrintedConjecture matches the printed conjecture is for a human reader |
| Paper | Human-readable manuscript | README: paper is not machine-checked |
| Improved bound | System improved the result twice | One theorem takes unformalized Agarwal–Ben-David FbsDegreeBound as a hypothesis |
| Stanford quote | Praise from Blanc, Docter, Strassle, Tan | Quote appears only on PSI’s page; no independent publication in our sources |
| Aaronson / Ambainis | — | No public comment found in listed sources |
What the conjecture is about
In plain terms, as PSI summarizes and as Aaronson and Ambainis set out in arXiv:0911.0996, the question is whether quantum computers can be exponentially faster on most inputs that lack special structure. Dramatic speedups such as Shor’s factoring rely on hidden patterns. The conjecture is a statement about low-degree bounded polynomials that represent a quantum algorithm’s acceptance probability after a limited number of queries: some input bit should have non-negligible “influence.” If that holds, classical algorithms can imitate the quantum yes-probability on most random strings with only a polynomial overhead in queries, not an exponential one.
Formalization and README caveats
PSI’s page says Lean accepted both the day-three proof and the final improved version. The public repository’s README states that four final theorems are proved with no placeholders or added axioms, and it describes static audits, axiom reports, kernel replay, a second kernel (lean4lean), and comparator runs. Those are PSI’s documented checks, not an independent rebuild by DailyMech.
The same README is explicit about limits that matter for readers: matching PrintedConjecture to the printed conjecture is left to a human expert; the paper itself is not machine-checked; one improved-bound theorem depends on an unformalized Agarwal–Ben-David hypothesis (FbsDegreeBound); and the mathematical statements, first paper draft, and formalization were produced by AI models in a harness developed by David Turturean at PSI, who reviewed the paper and is responsible for its correctness. PSI also lists Jim Halverson as auditing the proof and Phiala Shanahan as commenting on the Lean formalization.
Stanford researchers, as relayed by PSI
PSI says Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle, and Li-Yang Tan proved a special case in August 2026 and have been reading the full proof while writing a shorter expert exposition. PSI quotes them calling it “a huge result” that resolves a decades-old conjecture. That quote appears on PSI’s research page; our sources do not include an independent post from those authors, and they include no comment from Aaronson or Ambainis.
What to watch
Expert confirmation that the Lean statement matches the printed conjecture; public commentary from Aaronson, Ambainis, or other complexity researchers; the Stanford exposition PSI says is in progress; journal or arXiv refereeing; and any Anthropic comment on the unnamed model.
More coverage is on our Artificial Intelligence hub.
How we reported this
Based on PSI’s November 6, 2026, research page and the public repository README, both fetched directly, plus arXiv:0911.0996 for background only. We did not re-run Lean builds. Peer review, Anthropic confirmation, and independent mathematician endorsement are not claimed because they are absent from these sources.
Published and fact-checked November 6, 2026.
Sources
- PSI, “A proof of the Aaronson-Ambainis conjecture,” November 6, 2026. https://psi.inc/research/aaronson-ambainis/
- GitHub, physical-superintelligence/aaronson-ambainis (paper + Lean). https://github.com/physical-superintelligence/aaronson-ambainis
- Repository README. https://raw.githubusercontent.com/physical-superintelligence/aaronson-ambainis/main/README.md
- Aaronson & Ambainis background: https://arxiv.org/abs/0911.0996
DailyMech used AI tools to help research and draft this article; it was fact-checked by our editors.