For eighteen years, the Aaronson-Ambainis conjecture sat among the central open problems of quantum computing theory — the question of whether quantum computers can be exponentially faster than ordinary ones when there is no special structure in the problem to exploit. On Friday, a physics research lab called Physical Superintelligence (PSI) announced it has been settled: the conjecture is now a theorem, and the proof was found by a research system running a non-public Anthropic model, within three days of starting the run.
🔍 THE BOTTOM LINE
A research lab says an unreleased Anthropic model, deployed as part of a human-built research system, produced a complete machine-checked proof of an 18-year-old conjecture about the limits of quantum speedups. If the result holds up under community scrutiny, it matters twice over: it fixes a theoretical boundary quantum computing researchers have worked around since 2008, and it is the strongest entry yet in the accelerating streak of AI-solved mathematics — this time not by a published flagship model, but by one nobody outside a handful of labs can even run.
What the conjecture actually says
The short version, as Business Insider’s Kelsey Vlamis covered it: the conjecture, posed by Scott Aaronson and Andris Ambainis in 2008, concerns when quantum computers can be significantly faster than classical ones. Most known dramatic quantum speedups — Peter Shor’s factoring algorithm being the famous case — exploit structure: a repeating pattern in the input that the quantum computer can find. Aaronson and Ambainis asked whether exponential speedups survive when the input is random, with no such pattern to grab onto.
Their answer, stated as a conjecture about polynomials: no. If true, it meant quantum computers are at most polynomially faster — an enormous but bounded advantage — on random inputs. Proving it required mathematics researchers had chipped away at for years, and the field had counted it among the central open problems of quantum complexity theory.
What PSI says happened
According to PSI’s announcement, researcher David Turturean developed a research system that ran on PSI’s own infrastructure, using instances of an unnamed, non-public Anthropic model. The system searched existing literature, proposed ideas, combined approaches and tested arguments. A complete proof emerged on the third day of the run — with a weaker bound than the final version — and, crucially, it was not just claimed: the proof was formalized in Lean, the proof assistant in which a software kernel mechanically verifies every logical step. The system then improved its own result twice, and Lean accepted both refinements.
This is the detail that separates the claim from most AI-maths hype. A proof accepted by Lean’s kernel is not a proof a model says is right; it is a proof whose every step has been mechanically checked against axioms. Hallucination does not survive that gate. The Stanford team of Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — who settled a special case of the conjecture in August 2026 — have been reading the full proof, sending comments, and are writing a shorter exposition for experts. Their verdict, per PSI: “This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups. Everything is brought together in a rather magical way.”
The proof builds on the threshold strategy of Shachar Lovett and Jiapeng Zhang, strengthens David Reimer’s Butterfly Lemma, and — notably — found that one mathematical claim in the Lovett-Zhang approach does not hold in its stated general form, replacing it with a different result.
What it means for quantum computing
As The Quantum Insider’s analysis lays out, the theorem is a limit on data reads, not total computing time: a classical algorithm can approximate a quantum algorithm’s yes-or-no answer on most random inputs without exponentially more accesses to the input. That does not kill quantum computing — moderate speedups and huge gains on structured problems like factoring remain untouched — but it kills the hope of blanket exponential advantage on unstructured problems, and it redirects algorithm research toward problems whose structure offers a genuine edge.
The practical corollary is uncomfortable for the quantum-utopian reading: the “quantum computer beats everything everywhere” futures were always the least grounded part of the field. Theory now says the exceptional cases are the ones that need exceptional structure. That is a sharper map than the field had last week.
The pattern this continues — and the part that is new
This is no longer the first such result, and Singularity.Kiwi has tracked the streak closely. An unreleased Anthropic model made progress on the Riemann zeta function in August (covered here), another formalized Fermat’s Last Theorem’s proof in Lean in eleven days (covered here), and OpenAI’s 722-paper maths dump and the Fields-medalist backlash it triggered showed what the same method does at industrial scale (covered here). OpenAI claimed the Navier-Stokes equations in September. Terence Tao’s verdict last month that mathematics’ “romantic era” is over has become the field’s shorthand for the shift.
What is new here is not the technique — it is the source. Every prior milestone on this streak came from a lab showcasing a model, typically a frontier release with a name and a marketing plan. PSI’s system ran Anthropic’s non-public model, the working engine inside the lab rather than its shop window — the same class of unreleased model that METR’s audit found Anthropic researchers using to accelerate their own research (covered here). The frontier of AI-assisted mathematics is being set by models that customers and researchers outside the labs cannot buy, test or reproduce. The public leaderboard is falling behind what is actually running.
There is also a quieter caveat, the same one that attaches to every one of these announcements: we are reading the lab’s own account. Interesting Engineering notes the result has not yet undergone full independent academic review — the Stanford team’s close reading is the strongest external validation so far, and a Lean-accepted proof is a far more checkable artefact than a claimed breakthrough, but the broader community will want to read the paper, run the proof and probe the bounds themselves. PSI has posted the manuscript on GitHub, which makes all of that possible in principle. Expect the verification cycle to be measured in weeks, not the eighteen years the conjecture stood open.
The compounding loop, measured
Set this alongside what else arrived this week. METR’s independent audit of Anthropic, published Thursday, measured benchmark growth running at 1.9x the historical rate with roughly 80% of the acceleration attributed to AI-assisted research (covered here). That report was about the future rate of AI progress. The PSI result is the same loop showing up in a neighbouring discipline: a lab’s private model, embedded in a human-built research system, cracking in three days a problem that organized human effort had not closed since 2008.
The quantum-computing content of the theorem is real and will be digested by complexity theorists for months. But the meta-result is the louder one: the unreleased models are now doing mathematics that the mathematical community cannot yet do, and the run that matters is not the one on the benchmark chart — it is the one running quietly on a lab’s own infrastructure, one Anthropic does not even have to confirm.
As of publication, Anthropic has not responded to requests for comment on which model was used, and PSI’s claim has not been independently reviewed beyond the Lean check and the Stanford team’s reading.
Sources: PSI · Business Insider · The Quantum Insider · Interesting Engineering
