An AI Proved an 18-Year-Old Quantum Conjecture in 3 Days. The Proof Checks Out. The Payoff Doesn’t.

Three days is how long an AI research system needed to prove a conjecture that had resisted the world's best mathematicians for 18 years, or 6,574 days, a calendar compression of 2,191 to 1. On November 6, Physical Superintelligence (PSI), a Cambridge startup that calls itself an AI-built physics lab, announced that its system, running instances of a non-public Anthropic model, had proved the Aaronson-Ambainis conjecture, and that Lean, a proof assistant that checks every logical step by computer, accepted it.

Two days later, Scott Aaronson, the University of Texas computer scientist who posed the conjecture with Andris Ambainis in 2008, weighed in on his blog Shtetl-Optimized. He has not understood the proof himself yet. He believes it is correct anyway, for two reasons: there is a Lean certificate, and human experts have already gone over it and written an exposition. He also listed three emotions: satisfied, disappointed that humans did not get there first, and fatigued by the endless wonders from Aladdin’s Cave.

PSI published everything the same day: a 60-page paper, a Lean 4 formalization of 9,454 lines holding 648 machine-checked theorems, and a repository that spells out exactly what the machines checked and what they did not. That honesty is what makes this story interesting, and it is also what limits it.

What the conjecture actually says

Strip away the quantum framing and the conjecture is a statement about polynomials, the kind of thing a bright undergraduate could state in one sentence. Take any polynomial in n yes-or-no variables, with degree at most d, whose values always stay between 0 and 1, and whose variance is at least some number ε. Then some single variable must have a large influence on the output, at least a polynomial function of ε and 1/d. In plain language: a low-degree function that actually varies cannot hide its sensitive inputs. Somewhere in the haystack there is always a lever.

Quantum computing enters through a back door: a quantum algorithm that reads its input T times has an acceptance probability described by a polynomial of degree at most 2T. If every such polynomial has an influential variable, a classical algorithm can hunt for that variable, read it, and repeat, simulating the quantum algorithm on most inputs with only polynomially many reads. Aaronson and Ambainis showed in their 2009 paper, published in Theory of Computing in 2014, that this conjecture would settle a question open since 1999: can quantum computers be exponentially faster than classical ones on random, unstructured inputs? A proof says no. Exponential speedups need structure, which is why Shor’s factoring algorithm works (the structure of periodic functions) and random guessing does not.

PSI’s theorem makes the bound concrete: some variable has influence at least (8√15 / 125π⁴) · ε^5/2 / d⁶, which is at least (ε/d)⁷. I checked the constant myself: 8√15 / 125π⁴ equals 0.0025446, which PSI rounds to about 0.0025, real arithmetic rather than a decorative number.

Seven near-misses in eighteen years

Nobody should mistake this for a problem that fell easily. Dinur, Friedgut, Kindler and O’Donnell proved a version with exp(d) instead of poly(d) in 2006, and Montanaro handled a special case in 2012. O’Donnell and Zhao reduced the problem in 2016. Then came the false alarm: in November 2019, Nathan Keller and Ohad Klein posted a claimed proof, Aaronson celebrated it on his blog, and Paata Ivanisvili found what looked like a fatal flaw in Lemma 5.3, so Keller and Klein retracted. Bansal, Sinha and Wolf made partial progress in 2022. Bhattacharya proved it for random restrictions in 2024. In August 2026, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan settled the parallel case, showing a quantum algorithm making t queries in d parallel rounds can be simulated classically with t^O(d²) queries, a result accepted at FOCS 2026. That same group is now writing the human-readable exposition of PSI’s proof.

PSI’s proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang in 2023, replacing the one inequality their plan left open with a new inequality built from a determinant pairing, related to David Reimer’s Butterfly Lemma from his proof of the van den Berg-Kesten conjecture. Two ingredients carry the numbers: every point of the cube admits a fractional certificate of total weight at most π²d², and the sum of absolute increments at any point is at most 4d². Human roles, per PSI’s own disclosure: the proof, the paper and the formalization were produced by AI models, while David Turturean built the research system, scoped the problem, prompted the first draft, reviewed the paper and takes responsibility for its correctness, and adviser Jim Halverson audited the proof. Aaronson says the model was an internal Claude model; PSI says a non-public Anthropic model, and Anthropic has not commented.

The exponent fell, and that matters more than it looks

PSI’s system did not just find one proof. It found three, each better than the last, with Lean rechecking every version. Across those iterations the exponent on (ε/d) fell from 11 to 7. That sounds like a footnote. Run the numbers and it is a trillion-fold improvement.

Take a concrete case: variance ε = 0.01, degree d = 10. With exponent 11, the guaranteed influence is (0.01/10)¹¹, or 10^-33. With exponent 7, it is (0.01/10)⁷, or 10^-21. PSI’s final theorem guarantees an influential variable a trillion times more influential than its first Lean-checked version did. A machine that improves its own result by twelve orders of magnitude in the same run is doing something no human team did in eighteen years, which is iterating without fatigue.

Guaranteed influence of the most influential variable (LITF calculation from PSI’s bound)
Variance ε	Degree d	Explicit bound 0.0025·ε^5/2/d⁶	Cleaner bound (ε/d)⁷
0.5	2	6.9 × 10^-6	6.1 × 10^-5
0.1	5	5.1 × 10^-10	1.3 × 10^-12
0.1	10	7.9 × 10^-12	1.0 × 10^-14
0.01	10	2.5 × 10^-14	1.0 × 10^-21
0.25	20	1.2 × 10^-12	4.8 × 10^-14

Stare at that table for a moment, because it contains the whole story in miniature. Every guaranteed influence is minuscule in absolute terms. A variable guaranteed to matter at the level of 10^-12 matters in the way a theorem matters, not in the way a tool matters. Existence is not usefulness.

Now the honest catch: the simulation costs 10¹⁶ queries

Here is the calculation no source I read bothered to run, and it is the one that decides what this result means. A quantum algorithm making T queries has an acceptance polynomial of degree d = 2T, and the influence-chasing classical simulation implied by the conjecture needs on the order of (d/ε)⁷ queries. Plug in ordinary numbers:

Classical queries implied by the (d/ε)⁷ simulation bound (LITF calculation)
Quantum queries T	Error ε	Classical queries (d/ε)⁷
10	0.1	1.28 × 10¹⁶
10	0.01	1.28 × 10²³
50	0.1	1.00 × 10²¹
100	0.01	1.28 × 10³⁰

Read that first row twice. To simulate a quantum algorithm that reads its input ten times, the bound PSI proved allows a classical algorithm that reads its input 12,800,000,000,000,000 times. Polynomial in principle. Absurd in practice. At a billion reads per second, the classical simulation of ten quantum queries would take about 148 days. For a hundred quantum queries at one percent error, it would take longer than the age of the universe, by a factor of roughly a trillion.

This is the theorem’s real content, and it cuts both ways. It proves that exponential quantum advantage on unstructured inputs is impossible in the query model, which is a genuine landmark for complexity theory. It does not hand anyone a classical algorithm worth running, and it says nothing at all about the places quantum advantage actually lives: structured problems like factoring, chemistry simulation, or sampling tasks, where the advantage claims are made and the money is spent. Pedro Domingos told his 137,000 followers on X that the proof means the dream of quantum supremacy is dead. Aaronson pushed back on his blog, and he is right. Supremacy was never a claim about random yes-or-no questions.

Limitations

No journal has peer-reviewed the paper, and the 60-page human-readable text is not machine-checked, only the Lean formalization is. Lean verifies that the formal theorem follows from Lean’s axioms; it does not verify that PSI’s 20-line Lean definition, called PrintedConjecture, says the same thing Aaronson and Ambainis wrote in 2008. PSI’s own repository says that match is for a reader to confirm, and the Stanford and MIT exposition now in progress is exactly that check, unfinished. PSI is a startup with an obvious interest in the headline. Anthropic has not commented on the model. Aaronson knew about the result weeks before the announcement and kept it secret under embargo, which is normal practice, but it means his public endorsement is not independent verification. Finally, the model is non-public and unnamed, so nobody outside PSI can rerun the three-day search. A proof can be verified line by line; a discovery cannot be reproduced. That is a strange epistemic position for a claimed landmark, and it is the price of doing science with a model nobody else can run.

Strongest case against

Steelmanned, the skeptic’s case has three legs, and each one is load-bearing. First, the statement check is still open, and history says it matters: the 2019 Keller-Klein proof collapsed on a single lemma, and a formal proof of the wrong statement would be a true theorem about a different problem. Until the Blanc group’s exposition lands, the claim rests on PSI’s word plus a Lean certificate for a definition most readers cannot parse. Second, the method is a black box. A three-day run on an unnamed model, on private infrastructure, with no public log of the search, is not an experiment anyone can repeat, and science without repeatability is a press release with better footnotes. Third, the bound itself is practically vacuous, as the table above shows: a polynomial guarantee of 10¹⁶ queries is a theorem about complexity classes, not a tool for anyone building anything. Put together, the skeptic says: an unverifiable process produced a formally verified proof of a statement nobody has yet confirmed matches the conjecture, with a bound nobody can use. Every clause of that sentence is true. It is also compatible with the proof being completely correct, which is why Aaronson’s position, belief without yet understanding, is the reasonable one.

What you can do

If you follow quantum computing, treat this as a complexity-theory result, not a hardware result. It changes no roadmap, no qubit count, and no timeline for a useful machine. When the next headline claims a proof killed quantum advantage, ask two questions before sharing it: does the result count queries or wall-clock time, and does it cover structured problems or only random inputs? If the answers are queries and random inputs, the headline is wrong. If you work in AI research, the practical lesson is narrower and more useful: Lean-style machine checking turns an AI’s output from an assertion into an artifact, and that is the real template here, a discovery pipeline where every claim arrives with a certificate a computer can recheck. Watch for the Blanc group’s exposition, which will be the first independent reading of what was actually proved, and watch whether PSI submits the paper to a journal, which would put the statement check through the slowest and most boring filter ever invented, peer review. Boring is the point.

Bottom line

An AI system proved an 18-year-old conjecture about the limits of quantum speedups in three days, Lean checked every step, and the conjecture’s own author believes it. That is a real event, and it is the first time a machine has closed a central open problem in theoretical computer science with a certificate anyone can recheck. It is also, by the arithmetic, almost entirely without practical consequence: the classical simulation the theorem guarantees would need 1.28 × 10¹⁶ queries to replace ten quantum ones, the formal statement still awaits human confirmation that it matches the 2008 conjecture, and the discovery run itself cannot be repeated by anyone outside PSI. A landmark for complexity theory, a shrug for everyone building quantum computers, and a warning for everyone writing headlines about either. Three days of compute closed eighteen years of mathematics. Understanding what was actually proved will take the humans a little longer.