Illustrative image: a Bloch sphere, the standard way to picture a qubit's state — the kind of quantum system the Aaronson-Ambainis conjecture is about. Image: Glosser.ca, via Wikimedia Commons (CC BY-SA 3.0).
📌 Key Highlights
- PSI announced the proof on 6 November 2026. The conjecture, posed by Scott Aaronson and Andris Ambainis, had been open since 2008.
- An internal research system running a non-public Anthropic model found a complete proof on the third day of its run. The Lean proof assistant then verified every step by computer.
- The result: on most random yes-or-no questions, an ordinary computer can mimic a quantum computer with only polynomially more reads of the input — no exponential advantage.
- The bound proved is concrete: some input bit has influence at least (v/d)^7, where v measures how much the polynomial varies and d is its degree.
- The honest limits: the paper is a preprint, not yet peer-reviewed, the AI model is not public so the run cannot be repeated, and the result limits input reads — not total running time.
What happened?
Physical Superintelligence (PSI), a Cambridge, Massachusetts laboratory that describes itself as an AI-native physics lab, published “A proof of the Aaronson-Ambainis conjecture” on 6 November 2026, with the 60-page paper and the full Lean formalization public on GitHub. The work was led by David Turturean, a member of PSI’s technical staff, who built the research system, chose the problem and ran it — and who reviewed the paper and takes responsibility for its correctness. Jim Halverson audited the proof, and Phiala Shanahan commented on the Lean formalization.
The conjecture dates to a 2008 lecture by Scott Aaronson and is counted among the central open problems of quantum complexity theory. PSI says its system had a complete proof during the third day of a run on the company’s own infrastructure, then improved the result twice, with Lean accepting the final version. The Stanford team that settled a special case of the problem in August 2026 has been reading the proof, has sent comments, and is writing a shorter exposition of it for experts. Their verdict, quoted by PSI: “This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups.”
The Aaronson-Ambainis conjecture, explained simply
Start with how computer scientists measure effort here: by counting looks — how many times a computer must read its input, a long string of 0s and 1s. An ordinary computer reads one bit per look. A quantum computer’s look can be spread in superposition over many positions at once, which is why it can sometimes need far fewer looks.
The famous example is Peter Shor’s 1994 factoring algorithm, which factors large numbers far faster than any known ordinary method. It works because the problem hides a repeating pattern, and the quantum computer finds how often it repeats. Like most dramatic quantum speedups known, Shor’s algorithm relies on structure — a promise that the input has a rare pattern.
Aaronson and Ambainis asked the opposite question: on a random string, which almost never has such structure, can a quantum computer still win by an exponential margin? They turned it into pure mathematics. The probability that a quantum algorithm answers “yes” after T looks is a polynomial in the input bits, of degree at most 2T. Their conjecture said that if such a polynomial varies enough, some single input bit must have a large influence on it — so an ordinary computer can hunt down those influential bits one by one and estimate the answer without reading everything.
Scott Aaronson, who posed the conjecture with Andris Ambainis in 2008. Image: Wikimedia Commons (public domain).
PSI’s own analogy makes it concrete: think of the polynomial as a dial wired to on-off switches, where each switch is one input bit. The conjecture says flipping some switch moves the dial’s reading by a useful amount, however many switches there are. The proof shows that some bit has influence at least c·v5/2/d6, with c about 0.0025 — which is at least (v/d)7. The consequence is the headline: an ordinary computer needs at most a fixed power of T looks to predict the quantum computer’s answer, not exponentially many.
How the Aaronson-Ambainis conjecture proof was found in three days
PSI’s system ran multiple instances of a non-public Anthropic model that scoured the literature, generated candidate lemmas and stitched together arguments, while human researchers curated the material and edited the exposition. The proof follows a plan laid out by Shachar Lovett and Jiapeng Zhang, who had left one inequality in their plan as a conjecture of its own. PSI replaced that inequality with a new one, proved by pairing up input settings one to one using a determinant — David Reimer’s Butterfly Lemma already gives a weaker pairing, and the new proof also limits how often paired settings agree on each switch.
The verification is the part that makes this more than a claim. The Lean development is complete: the theorems are proved with no placeholder and no added axiom, and they were re-checked by two independent implementations of the Lean kernel, plus a Rust type checker in a comparator run. The Lean version is pinned (Lean 4.33.0, Mathlib v4.33.0), and the only axioms behind the final theorems are the three standard Lean principles. PSI is open about what the machine checks do not cover: a reader still has to confirm that the formal statement says what the conjecture says, and the 60-page paper itself is not machine-checked.
What the proof does — and does not — do
| Claim | Status |
|---|---|
| Exponential quantum speedup on random yes-or-no questions | Ruled out — in the query model, which counts input reads |
| Exponential speedups on structured problems, such as Shor’s factoring | Unaffected — structure is exactly what the theorem requires |
| Total running-time advantage of quantum computers | Not addressed — the result counts looks at the input, not total work |
| Peer review | Not yet done — preprint, with no independent expert assessment published as of 7 November |
| Repeating the AI’s three-day run | Not possible — the Anthropic model used is non-public |
Why it matters
The result draws a sharper map of where quantum advantage can actually come from. If exponential speedups need structure, then algorithm designers, research labs and funders should focus on problems with exploitable patterns — periodicity, symmetry, hidden structure — rather than hoping quantum hardware will beat classical machines on arbitrary data. That is a practical steer for a field that has spent years debating which problems are worth a quantum computer at all. For readers in India following quantum computing — a growing research area here, from university theory groups to the national quantum mission’s industry push — it clarifies which claims about quantum advantage deserve scepticism and which deserve attention.
There is a second story here, about how mathematics gets done. In September, OpenAI said an AI system had solved a 90-year-old problem, the Navier-Stokes equations. Now an AI system has produced a machine-checked proof of an 18-year-old conjecture. The pattern is becoming hard to ignore: AI is moving from answering questions to settling open ones, with a proof assistant as the referee. That does not make the human mathematicians redundant — PSI’s own account stresses human curation, auditing and responsibility — but it changes what a small team can attempt.
Should you care?
Update: Aaronson responds — he believes the proof is correct (8 November)
Two days after PSI's announcement, Scott Aaronson himself weighed in. In a post on his blog Shtetl-Optimized on Sunday 8 November 2026, Aaronson wrote that he believes the proof is correct, for two reasons: there is a Lean certificate, and human experts have already gone over the proof and understood it. He also pointed readers to a "beautiful-looking exposition" of the proof written by Guy Blanc of MIT and Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford — the team that proved the special case in August.
Aaronson revealed that PSI told him about the result several weeks before the announcement, and he had to keep it secret until then. He also named the model family behind the proof: where PSI described only a "non-public Anthropic model", Aaronson wrote that the proof was obtained using PSI's proprietary research harness on "an internal Claude model".
He used the post to correct a misconception spreading online: the result rules out only one particular type of quantum supremacy — exponential speedups for yes-or-no problems relative to random oracles, which he and Ambainis had already conjectured did not exist. It has zero effect on Shor's factoring algorithm, which uses a highly non-random (periodic) oracle, and zero effect on simulating quantum physics and chemistry. He also noted the 2022 Yamakawa–Zhandry breakthrough, which showed exponential quantum speedups are possible for NP search problems relative to random oracles. His own feelings, he wrote, were mixed: satisfied the conjecture turned out to be true, disappointed humans did not get there first, and fatigued by the pace of longstanding problems falling.
What is still open: the paper has not been through journal peer review, and Aaronson himself writes that he has not yet understood the proof — he is relying on the Lean certificate and on the experts who have read it.
FAQs
What is the Aaronson-Ambainis conjecture?
A statement from 2008 by Scott Aaronson and Andris Ambainis about polynomials: if a low-degree polynomial bounded between 0 and 1 varies enough, some single input variable must have a large influence on its value. It matters because it decides whether quantum computers can be exponentially faster than ordinary ones on random inputs — and the new proof says they cannot, in the query model.
Did AI really prove the Aaronson-Ambainis conjecture?
PSI’s research system, running a non-public Anthropic model, found the proof in three days, and the Lean proof assistant verified every step by computer. Humans led the work, curated the material and take responsibility for it. The paper is a preprint and has not yet been peer-reviewed, so independent expert assessment is still to come.
Does this mean quantum computers are useless?
No. The result limits exponential speedups on random, unstructured inputs when effort is measured by input reads. Structured problems — Shor’s factoring algorithm is the classic example — keep their exponential advantage, and the theorem says nothing about total running time, memory or other resources.
What is the Lean proof assistant?
Lean is software in which a mathematical proof is written so that a computer checks every logical step. If Lean accepts a proof, the formal statement is correct as written — which is why PSI’s Lean formalization, with no placeholders and no added axioms, carries more weight than a paper alone. The catch is that Lean checks the formal statement, not whether it matches the conjecture as printed, so a human still has to confirm that match.
Takeaway
An 18-year-old question in quantum computing now has an answer — found by an AI system in three days, with a machine-checked receipt. Quantum computers keep their edge where problems have structure; on random problems, the edge was never really there. If you want the details, read PSI’s announcement and the public Lean code — and watch for the Stanford team’s shorter exposition for experts, which is the next thing to look out for.
For more on this week’s quantum research, read our explainers on Oxford’s Aharonov-Bohm trapped-ion experiment and Rydberg-atom error correction, and our look at Fudan’s D3D speculative decoding, which speeds up AI models in a very different way.
Sources
- Physical Superintelligence — A proof of the Aaronson-Ambainis conjecture (primary source, published 6 November 2026)
- PSI on GitHub — Paper and Lean 4 formalization of the proof (primary source)
- The Quantum Insider — AI-Assisted Proof Settles Longstanding Question About Quantum Speedups (independent reporting, 6 November 2026)
- Aaronson & Ambainis — The Need for Structure in Quantum Speedups (arXiv:0911.0996) (the original conjecture)
- Scott Aaronson — Aaronson-Ambainis Conjecture proved! (By AI, of course) (Shtetl-Optimized) (the conjecture's co-author responds, 8 November 2026)
- Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — Exposition of the Aaronson–Ambainis proof (PDF) (expert exposition of the proof)
Comments
Post a Comment