An AI System Proved a 2008 Quantum Conjecture in Three Days, but the Model Behind It Has No Name
PSI says an AI system produced a Lean-checked proof of the Aaronson-Ambainis conjecture in three days, but the Anthropic model is unnamed and run logs are missing.
Physical Superintelligence, a research lab that trades as PSI, said on 6 November that an internal AI research system proved the Aaronson-Ambainis conjecture, a quantum complexity question open since 2008. The system ran instances of a non-public Anthropic model. PSI says it had a complete proof on the third day, and that Lean accepted the final version.
The conjecture connects a pure maths statement about polynomials to a practical question: when can a quantum computer be exponentially faster than a classical one? Aaronson and Ambainis showed that if their conjecture held, quantum computers cannot get an exponential advantage on random inputs unless those inputs contain a rare structure. Shor’s algorithm is the famous exception, because factoring hides a repeating pattern.
The catch is the evidence around the result, not the mathematics. PSI published the paper, the Lean code and a detailed verification log, more than most AI research announcements offer. It did not publish the model name, prompts, token count, cost or run transcripts. No outside mathematician has signed off yet, although the Stanford group that proved a special case in August says it is reading the manuscript.
Quick answer: PSI says an AI system running a non-public Anthropic model proved the Aaronson-Ambainis conjecture in three days and that Lean accepted the result. The proof shows every bounded polynomial of degree d with variance epsilon has a variable with influence at least (epsilon/d) to the seventh power. That resolves a 2008 conjecture and limits exponential quantum speedups on random inputs in the query model. It does not make quantum computers useless, does not cover runtime, and the model is unnamed. Lean checked the formal statement, not whether it matches the informal conjecture word for word.
What PSI actually proved
The conjecture concerns bounded polynomials of low degree on the Boolean cube. The influence of a bit is the average squared change in a polynomial’s value when that bit is flipped.
Aaronson and Ambainis conjectured that if the polynomial varies enough across inputs, some bit must have large influence, with a bound that shrinks only polynomially as degree rises. PSI’s proof gives an explicit constant of about 0.0025 and a final bound of (epsilon/d) to the seventh power.
A quantum algorithm’s acceptance probability is a polynomial of degree at most twice its query count. Large influence lets a classical machine find that bit, learn the polynomial and predict the answer without exponentially many queries. The new bound makes that work for every bounded low-degree polynomial.
Three days, with no trace of the run
PSI says the system had a complete proof on day three, then improved the result twice while working on related problems. Lean accepted the final version each time. That is fast for a problem that has resisted specialists for 18 years.
It is also unverifiable from the outside. The repository has the paper, the Lean development, build logs and verification notes, but no run transcript, prompt log, token budget, cost estimate or model identifier. PSI calls the model only a non-public Anthropic model.
The accountability chain is narrow. PSI says the mathematical statements, first draft and Lean formalization were produced by AI models in a harness built by David Turturean, a member of technical staff, who reviewed the paper and is responsible for its correctness. Jim Halverson audited the proof. Phiala Shanahan commented on the formalization. That is internal review, not peer review.
How it compares with earlier work
| Result | Date | Scope | Key bound | Machine checked |
|---|---|---|---|---|
| Nisan and Szegedy | 1994 | Boolean-valued polynomials | Degree bound for a special class | Not stated |
| Dinur, Friedgut, Kindler and O’Donnell | 2007 | Bounded functions on the cube | Decays exponentially in degree | Not stated |
| Blanc, Docter, Strassle and Tan | August 2026 | Quantum algorithms with fixed parallel rounds | No exponential speedup in that model | Not stated |
| PSI, Turturean | 6 November 2026 | All bounded polynomials of degree d | At least (epsilon/d) to the seventh, explicit constant about 0.0025 | Yes, Lean 4.33 |
Source: PSI research page and paper, 6 November 2026. The table lists only results cited in that paper.
The difference is the exponent: a bound that decays exponentially in degree cannot support the simulation argument for arbitrary degree, while a polynomial bound can.
Lean checks the proof, not the question
The formal verification is the strongest part. The repository uses Lean 4.33.0 and Mathlib v4.33.0 and proves four public theorems. PSI says the sources contain no sorry, no axiom and no unsafe declarations, and that the theorems use only the standard axioms propext, Classical.choice and Quot.sound.
The checks go beyond a normal build. PSI replayed every declaration through the Lean kernel and repeated the replay with lean4lean, an independent type checker. A comparator checked the four theorems against a challenge file that imports only the conjecture statement. A deliberately false control project was rejected.
But Lean verifies that the proof proves the formal statement, not that the formal statement is the conjecture as mathematicians understand it. PSI’s trust boundary says the statement, the paper and the foundations are not machine checked. That is a higher bar than most AI maths claims clear. Sections including the consequences and proof overview have no Lean counterpart, and those sections carry the quantum interpretation.
Today Physical Superintelligence PBC is announcing a proof of the Aaronson-Ambainis conjecture, one of the central open problems in quantum complexity, with major implications for quantum computing speedup.https://t.co/sAewkKdSOu
Thread 👇
— Physical Superintelligence (@psipbc) November 6, 2026
What the result does not say
It does not say quantum computers are only polynomially faster for every problem. The statement is about query complexity and inputs with no rare structure. Runtime can still differ enormously, and structured problems such as factoring still admit exponential speedups.
It also does not settle the practical case for quantum hardware. A polynomial query advantage can still be valuable, and the theorem does not rule out exponential advantages from depth, promise problems or other structure. Quoting this as the end of quantum computing is overreading it.
Ah, another beautiful question in quantum complexity theory solved! This one is due to Scott Aaronson and @AAmbainis, about the necessity of structure in a problem for exponential quantum advantage. This question inspired a lot of research and we collectively learned a lot about… https://t.co/jkqOJBBBpQ
— Henry Yuen (@henryquantum) November 6, 2026
A lab with an interest in the headline
PSI is a public benefit corporation with more than $58 million in funding, led by Breakthrough Energy Ventures, and 25 or more researchers and engineers. It calls itself an AI-native physics lab where verification is central, so a machine-checked proof is a natural flagship result.
The commercial interest does not make the proof wrong, but it explains the framing. A lab selling autonomous scientific discovery benefits from a three-day proof of an 18-year-old conjecture. The Anthropic connection is less clear: the model is unnamed, so Anthropic gets a notable association without a model card or benchmarks.
What it means for Indian developers
The direct impact is limited. Indian teams cannot rent the model, reproduce the run or inspect the checkpoint, and no API price or deployment option changes this quarter.
The useful lesson is the verification stack. PSI shipped Lean code, a second kernel replay, a comparator and recorded digests instead of asking readers to trust a PDF. Indian teams building high-stakes systems can copy that pattern, especially in finance, health and government work.
That creates a talent question. Lean and formal methods skills are scarce, and the tooling assumes a research culture most services companies lack. Teams that invest in proof engineering will make stronger correctness claims than teams that rely on evaluation scores.
Confirmed versus not confirmed
| Claim | Status | Evidence |
|---|---|---|
| PSI announced a proof on 6 November 2026 | Confirmed | PSI page and public repository |
| The proof was complete on day three | Not independently confirmed | PSI statement only; no run logs |
| Lean accepted the final proof | Confirmed in the repository | Lean 4.33 and kernel replays |
| A non-public Anthropic model was used | Confirmed by PSI, model unidentified | No name or system card |
| The formal statement matches the original conjecture | Not independently confirmed | PSI says a reader must verify this |
| Outside mathematicians validated the full proof | Not confirmed | Stanford group is still reading it |
| The result rules out exponential quantum speedups in general | Not confirmed | It covers query complexity, not runtime |
| Cost and compute for the run are known | Not confirmed | PSI did not disclose either |
FAQ
Did an AI really prove the Aaronson-Ambainis conjecture?
PSI says its system produced a complete proof that Lean accepted, and the paper and code are public. No independent review has been published, so it is a strong, machine-checked preprint rather than settled consensus.
What is the Aaronson-Ambainis conjecture?
It says that a bounded polynomial of low degree on the Boolean cube, if it varies enough, must have some input bit with large influence. Aaronson and Ambainis showed this implies no exponential quantum speedup on random inputs in the query model.
Does this mean quantum computers are not faster than classical computers?
No. The result is about query complexity and inputs without rare structure. Shor’s algorithm still gives an exponential speedup for factoring because factoring has structure. The theorem narrows the landscape of exponential advantages without eliminating them.
Can I check the proof myself?
Yes. PSI published the paper, the Lean code and verification notes on GitHub, with build and replay instructions.
Which Anthropic model was used?
PSI has not named it. The company describes it only as a non-public Anthropic model used on PSI’s own infrastructure.
Sources
Physical Superintelligence, A proof of the Aaronson-Ambainis conjecture, 6 November 2026.
David Turturean, Paper, Lean formalization and verification notes, 6 November 2026.
Scott Aaronson and Andris Ambainis, The Need for Structure in Quantum Speedups, Theory of Computing 10 (2014), 133-166.
Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan, Quantum Speedups Require Structure or Depth, August 2026.
Physical Superintelligence, Lab overview and funding disclosure, accessed 7 November 2026.
Earlier coverage: OpenAI’s Astra and ten open maths problems, Anthropic’s NIST P-256 seed claim, and llm-d 1.0 and the vendor demo problem.