Aaronson-Ambainis conjecture proved: an unreleased Anthropic model settles the 18-year-old quantum question, Lean-checked

Originally published at https://aifrontierpost.com/articles/psi-anthropic-aaronson-ambainis-conjecture-proof/

An AI research system running an unreleased Anthropic model has proved the Aaronson-Ambainis conjecture, an 18-year-old open problem in quantum computing — and the Lean proof assistant has verified every step of the argument.

TL;DR: Physical Superintelligence (PSI) announced on November 6, 2026 that its research system, running a non-public Anthropic model, found a proof of the Aaronson-Ambainis conjecture, open since 2008. The Lean proof assistant accepted the proof — and the final version after the system improved the result twice — and the manuscript and Lean formalization are public. It has not been peer reviewed.

Who: Physical Superintelligence (PSI), an AI-native physics lab; its research system ran instances of a non-public Anthropic model. David Turturean led the work.

What: A proof of the Aaronson-Ambainis conjecture, which had been open since 2008 and is counted among the central open problems of quantum complexity theory.

When: Announced November 6, 2026. The system had a complete proof during the third day of a run on PSI's own infrastructure.

Verification: The Lean proof assistant accepted the proof, and accepted the final version after the system improved the result twice. The manuscript and Lean 4 formalization are public.

The bound: The proof shows some bit has influence at least c·v5/2/d6, where c is about 0.0025 — at least (v/d)7.

Caveat: The proof has not been peer reviewed, and experts still need to confirm the formal statement Lean checked matches the original conjecture.

Physical Superintelligence (PSI) announced on November 6, 2026 that a research system it developed internally has proved the Aaronson-Ambainis conjecture, settling a question about quantum computing that has been open since 2008. The system ran instances of a non-public Anthropic model — PSI has not named the model — and had a complete proof during the third day of a run on the company's own infrastructure. The Lean proof assistant, software that checks every step of a mathematical argument by computer, accepted it.

The conjecture, posed by computer scientists Scott Aaronson and Andris Ambainis, bears on a basic question: when can quantum computers be exponentially faster than ordinary ones? Dramatic quantum speedups, like Peter Shor's 1994 factoring algorithm, rely on structure — a promise that the input hides a rare pattern. Whether quantum computers can be exponentially faster on random inputs, which almost never have such structure, was unknown. Aaronson and Ambainis found a way to settle it with pure mathematics: they stated a conjecture about polynomials and showed that, if it is true, quantum computers are at most polynomially faster on random inputs.

How the proof was found

PSI says the system found the proof, then was set to work on related open problems. Along the way it improved the result twice, and Lean accepted the final version. The proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang, who had left one inequality of their plan as a conjecture; PSI's proof replaces that conjectured inequality with a new one, proved in the manuscript, using a pairing argument that builds on David Reimer's Butterfly Lemma.

The work was led by David Turturean, a member of PSI's technical staff, who developed the research system, scoped the problem, prompted the model to package the results into a first draft, reviewed the draft and is named as responsible for the paper's correctness. Jim Halverson, a PSI adviser, audited the proof, and Phiala Shanahan, another adviser, commented on the Lean formalization. PSI says the mathematical statements, the first draft of the paper and the Lean formalization were produced by AI models.

The manuscript and the Lean 4 formalization are public, so anyone can replay the encoded argument. A Stanford group — Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — had settled the conjecture's prediction in a special case in August 2026, and has been reading PSI's proof of the full conjecture. The group called it "a huge result" that "resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups," and is writing a shorter exposition of it for experts.

What it does — and does not — settle

The proof's headline bound is concrete: if a polynomial's reading varies by an amount v and its degree is d, some bit has influence at least c·v5/2/d6, where c is about 0.0025 — at least (v/d)7. In plain terms, an ordinary computer can now predict a quantum computer's probability of answering yes, up to a small error, for all but a small fraction of random strings, with the number of input reads growing at most like a fixed power of the quantum computer's reads — not exponentially. On yes-or-no questions about random inputs, a quantum computer cannot save exponentially many looks unless the input has a rare pattern.

That is a result about limits, not about building quantum computers: it says nothing about structured problems like factoring, where quantum speedups remain. And the verification has explicit limits. The proof has not been peer reviewed, the human-readable paper is not itself machine-checked, and a reader must still confirm that the formal statement Lean verified matches the printed conjecture. Unite.AI's report of the announcement notes the same caveats: the formal development contains no proof placeholders or added axioms, and its declarations were replayed through Lean's kernel and through lean4lean, an independent implementation of Lean's type checker.

Why this proof matters

The result is two stories at once. For quantum computing, it closes one of the field's central open problems and draws a clean boundary: exponential advantage needs structure. For AI, it is a machine-checked proof of a problem that had resisted human mathematicians for 18 years, produced by a model the public cannot use — a reminder of how far internal research systems have moved past what is publicly available. Independent assessments of Anthropic's research pace have pointed the same way: METR estimated in November that Anthropic's AI capabilities are improving at roughly twice the rate of an earlier period, with AI itself responsible for much of the acceleration.

Whether the proof survives expert scrutiny is now the open question — and the one that will decide whether November 6, 2026 goes down as the day a conjecture became a theorem, or the day a machine-checked argument still needed a human to say what it proved. The formalization is public, the kernel has spoken, and the mathematicians are reading.

Frequently asked questions

What is the Aaronson-Ambainis conjecture?

A 2008 conjecture by Scott Aaronson and Andris Ambainis about polynomials, which implies that quantum computers can be at most polynomially faster than ordinary computers on random inputs — the inputs that almost never carry the structure quantum speedups rely on.

Was the proof checked by a human or a machine?

By a machine: the Lean proof assistant accepted the proof, and accepted the final version after the system improved the result twice. It has not been peer reviewed, and experts still need to confirm that the formal statement Lean checked matches the original conjecture.

Which Anthropic model proved it?

PSI has not named the model. It describes it only as a non-public Anthropic model, and says instances of it ran inside PSI's own research system on the company's infrastructure.