The Aaronson-Ambainis Conjecture and an AI-Run Proof
On November 6, Physical Superintelligence (PSI) posted a manuscript and a Lean 4 formalization claiming a proof of the Aaronson-Ambainis conjecture, a problem in quantum complexity theory that has been open since 2008. PSI says the proof came from an internal research system running instances of a non-public Anthropic model on the company's own infrastructure, and that the system had a complete proof during the third day of the run.
The question
Shor's factoring algorithm and Simon's algorithm achieve exponential speedups in the query model, but both depend on inputs with strong global structure, such as a periodic function. Scott Aaronson and Andris Ambainis asked what happens without that structure. If a quantum algorithm makes T queries to an input string, can a classical algorithm approximate its acceptance probability on most inputs using only polynomially many queries in T?
They reduced the question to a statement about polynomials. Beals and coauthors had shown that the acceptance probability of a T-query quantum algorithm is a polynomial of degree at most 2T that stays between 0 and 1 on every input. Aaronson and Ambainis conjectured that every such bounded, low-degree polynomial with non-trivial variance has a variable with large influence, meaning that flipping that one input bit changes the output noticeably on average. If that holds, a classical algorithm can keep querying the most influential bit and approximate the quantum one with polynomial overhead.
Partial results accumulated for years. Dinur, Friedgut, Kindler and O'Donnell proved a version in 2006 with a bound that decays exponentially in the degree. Montanaro proved a special case in 2012, and Bansal, Sinha and de Wolf covered completely bounded block-multilinear forms in 2022. In 2019 Nathan Keller and Ohad Klein posted a claimed proof, which they retracted after Paata Ivanisvili found a flaw in one lemma. In August 2026, a Stanford group of Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan proved the consequence for quantum algorithms that query in a fixed number of parallel rounds.
What PSI claims
The manuscript, credited to PSI's David Turturean, states that if a polynomial of degree d takes values in [0,1] and has variance v, some variable has influence at least 8√15/(125π⁴) · v^(5/2)/d^6. The constant works out to about 0.0025, and the bound implies the simpler form (v/d)^7. Earlier general bounds decayed exponentially in d. For yes-or-no questions on random inputs, the result means a classical simulation needs at most a fixed power of T queries. It places no new limit on quantum speedups for structured problems such as factoring.
The proof follows a strategy Shachar Lovett and Jiapeng Zhang laid out in a 2022 paper on fractional certificates, which reduced the conjecture to inequalities they could not prove. PSI's argument replaces one of those with a new inequality built on a pairing of inputs generated by a determinant. PSI describes it as a strengthening of David Reimer's Butterfly Lemma that also limits how often paired inputs agree on each coordinate.
According to PSI, the first complete proof had a weaker bound. The company then pointed the system at related open problems, and it improved the result twice. AI models produced the mathematical statements, the first draft and the Lean formalization. Turturean scoped the problem, ran the system, reviewed and edited the paper, and takes responsibility for its correctness. Advisor Jim Halverson audited the proof, and Phiala Shanahan commented on the formalization.
What Lean checks
The repository at github.com/physical-superintelligence/aaronson-ambainis includes the paper, the Lean library and audit notes. It reports that the four final theorems depend only on Lean's three standard axioms, that a static audit finds no sorry placeholders, and that declarations were replayed through Lean's kernel and through lean4lean, a separate type checker. A single-threaded replay took about 11 minutes and 7.4 GB of memory, which puts an independent rerun within reach of anyone with a Linux machine.
The repository also states its limits. A reader must confirm that the formal statement, PrintedConjecture, matches the conjecture as Aaronson and Ambainis wrote it. The human-readable paper is not machine-checked, and one of the four final theorems depends on a hypothesis from Agarwal and Ben-David that is not formalized.
Reception so far
Blanc, Docter, Strassle and Tan have read the full proof, sent comments, and are writing a shorter exposition for specialists. In a statement PSI published, they called it "a huge result." FourWeekMBA reported finding no public assessment yet from Aaronson or Ambainis, and PSI's materials do not mention a journal submission. The Stanford exposition, and a check by outside readers that PrintedConjecture says what the 2008 conjecture says, are the open items.
About the author
David Borish is the author of The Tony Hawk Paradox: When Video Games Predict Reality. More of his writing is at davidborish.com
