Aaronson–Ambainis conjecture

Proof claimed · 06 Nov 2026

A proof of the Aaronson-Ambainis conjecture

“The Aaronson-Ambainis conjecture is now a theorem. … Now, a research system developed internally at Physical Superintelligence (PSI), running a non-public Anthropic model, found a proof for it, settling one of the most fundamental questions in quantum computing.”

By

David Turturean (PSI, Physical Superintelligence)

AI involvement

At PSI, we found the proof with a research system we developed internally, in a run on our own infrastructure. Instances of a non-public Anthropic model were used in the run. … David Turturean, Member of Technical Staff, led this work: he developed the research system, scoped the problem and ran the system on it, then prompted the model to package the results into a first draft of the paper, reviewed the draft and is responsible for the paper’s correctness.

Model

a non-public Anthropic model (not named in the post), as stated

Where

PSI website (research post), with paper PDF and Lean repository

Write-up

Natural language, published by the source

Formal proof

Lean 4, published by the source

Repository

physical-superintelligence/aaronson-ambainis at 2a6ceae · read 11 Nov 2026

Statement file

AaronsonAmbainis/Conjecture.lean

Source last read

07 Nov 2026

Note: The repository README says: “The mathematical statements, the first draft of the paper and the Lean formalization were produced by AI models, in a research harness developed by David Turturean at PSI.” Per the post, Jim Halverson audited the proof. The README says the Lean theorems were re-checked by two independent implementations of the Lean kernel, and that whether the Lean statement says what the conjecture says “is for a reader to confirm”. Preprint; not peer reviewed.

Checks

2 reviews · 1 exposition · 1 comment

• 06 Nov 2026 · Review · Jim Halverson (PSI advisor) (as reported by the claimant): An audit of the proof by an advisor of the claimant, as stated in the claimant's research post; the post gives no details of the audit and links no report by the auditor. “Jim Halverson, Advisor, audited the proof.” Source
• 06 Nov 2026 · Review · Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan (Stanford University) (as reported by the claimant): Reading of the full proof, with comments sent to the claimant and a shorter exposition in preparation, as stated in the claimant's research post, which also quotes the group's praise of the result. No report by the group is linked from the post. “They have since been reading our proof of the full conjecture, have sent us comments and are writing a shorter exposition of it for experts.” Source
• 08 Nov 2026 · Exposition · Guy Blanc, Jordan Docter, Carmen Strassle, Li-Yang Tan (arXiv:2611.11626): A 30-page exposition of the proof organized in four main steps, with parameters not optimized and weaker exponents than the original. The abstract page states no verdict on correctness. “The proof was then shared with the authors, who worked to understand it and prepare this exposition.” Source
• 09 Nov 2026 · Commentary · Thomas Huffstutler, David Miloschewsky, Supartha Podder (arXiv:2611.12795): An independent short proof of the conjecture via the completion framework. Per the abstract, the only ingredient taken from Turturean's proof is a special case of his certificate inequality, for which the paper gives its own self-contained argument; no check of the rest of his argument is stated. “The only result we use from Turturean's recent proof is a special case of his certificate inequality, for which we provide a self-contained proof.” Source