- PSI says a system built around an unreleased Anthropic model found a full proof of the 2008 Aaronson-Ambainis conjecture on day 3 of a run, then strengthened the result twice, with every version accepted by the Lean proof checker.
- The result means quantum computers cannot be exponentially faster than ordinary computers on yes-or-no questions about random inputs; dramatic speedups like Shor's algorithm need structure in the data.
- Stanford researchers who proved a special case in August called it “a huge result,” though the paper has not yet been through journal peer review and Anthropic has not named the model.
Physical Superintelligence (PSI), an AI-native physics research lab, said on November 6 that its internal research system, running instances of a non-public Anthropic model, produced a complete proof of the Aaronson-Ambainis conjecture on the third day of a single run. The conjecture, stated in 2008 by Scott Aaronson and Andris Ambainis, is one of the central open problems in quantum complexity theory, and the Lean proof assistant, which checks every logical step by computer, accepted the proof.
A non-public Anthropic model produced a Lean-checked proof on day three
PSI ran the search on its own infrastructure, and the company's research announcement says the system reached a complete proof during the third day. PSI then pointed the same system at related open problems, and it improved the bound twice before Lean accepted the final version. The final theorem shows that in any non-constant bounded polynomial of degree d with variance v, some single input bit has influence of at least about 0.0025 times v to the power 2.5, divided by d to the power 6. Earlier general bounds weakened exponentially as the degree grew.
The proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang, who had left one inequality as an open conjecture. PSI's system replaced it with a new inequality, proved through a one-to-one pairing of input settings built from a determinant, which extends David Reimer's Butterfly Lemma. PSI's David Turturean built the system, scoped the problem and takes responsibility for the paper's correctness, while advisor Jim Halverson audited the proof. The manuscript and the complete Lean formalization are public.
| Year the conjecture was stated | 2008 |
| When PSI's system had a complete proof | Day 3 of the run |
| Later improvements to the bound | 2, each accepted by Lean |
| Constant in the final influence bound | About 0.0025 |
Quantum speedups on random data are now proven to have a ceiling
The conjecture matters because Aaronson and Ambainis showed it would settle when quantum computers can win big. Shor's factoring algorithm gets an exponential speedup because the input hides a repeating pattern. With the conjecture proven, an ordinary computer can predict a quantum algorithm's yes-or-no answer on almost all random inputs while reading only polynomially more bits, so any exponential advantage has to come from structure in the problem.
The machine check carries extra weight on this problem. In 2019 a human-written proof was posted and withdrawn within weeks after a reader found a fatal flaw in one lemma. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford, who settled a special case in August, are now writing a shorter exposition of PSI's proof for experts.
“This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups.”
Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Stanford University, as published by PSI, November 6, 2026
The announcement lands a day after METR reported that AI now drives most of Anthropic's doubled pace of progress, and it follows Claude's 11-day formalization of Fermat's Last Theorem and OpenAI's claimed disproof of a 1999 computing hypothesis. PSI's result goes further than formalizing known mathematics, because it closes a question that specialists had worked on for nearly two decades. Lean guarantees the formal statement is proven, and the remaining human check is whether that statement matches the conjecture as Aaronson and Ambainis meant it.
The deeper shift is who now sets the pace of theoretical computer science. A small lab with access to an unreleased reasoning model closed an 18-year-old problem in a three-day run, and the experts' job moved from finding the proof to reading it, which means the next bottleneck in mathematics is human review capacity.
Santage is committed to independent, transparent journalism. This article is produced in accordance with Santage's Editorial Standards and aims to provide accurate and timely information. Readers are encouraged to verify information independently.