PSI claims Lean-checked proof of the Aaronson–Ambainis conjecture
Awaiting review
Importance: historic (5 of 5)The takeaway
On 6 Nov 2026 the startup Physical Superintelligence PBC (PSI) announced a proof of the Aaronson–Ambainis conjecture, a central open problem of quantum query complexity since 2008: every bounded low-degree polynomial on the Boolean cube has an influential variable.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Historic (5 of 5)
- Last verified
- 9 November 2026
Your AI and this story
- GPT-6 Astra190 days after its cutoff
- Claude Opus 5.5129 days after its cutoff
- Gemini 4 Argon220 days after its cutoff
- Grok 4.7159 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 129 days before it.
Key facts
- Reactions by 8 Nov: none from Scott Aaronson or Andris Ambainis. Readers posted the PSI link under Aaronson’s 2019 post on the conjecture and under his newest post (6 Nov comments, ‘Thoughts on https://psi.inc/research/aaronson-ambainis/1 ?’); no reply. Web search finds no expert assessment
- Claim (PSI): if a bounded, non-constant polynomial of degree d has variance v, some input bit has influence at least c·v^(5/2)/d^6 with c = 815/(125π⁴) ≈ 0.0025, which is at least (v/d)^7; this is the Aaronson–Ambainis conjecture up to the polynomial form of the bound
- Consequence: quantum algorithms are at most polynomially faster than classical ones on most inputs of unstructured (random) yes/no problems (‘quantum speedups need structure’)
- Method: builds on a plan of Shachar Lovett and Jiapeng Zhang, replacing one of their conjectured inequalities with a newly proved one
- AI: PSI’s internal research system on its own infrastructure, running instances of a non-public Anthropic model; complete proof on the third day; the system then improved the bound twice
- Verification: the first complete proof and the final version were accepted by Lean (repository published); Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan (Stanford) read the proof: ‘This is a huge result. It resolves a decades-old conjecture with important implications.’ They are writing a shorter expository version
- People: David Turturean (PSI technical staff) scoped the problem, ran the system, had the model draft the paper and takes responsibility for correctness; advisers Jim Halverson audited the proof and Phiala Shanahan commented on the Lean formalization
- History: Keller and Klein’s 2019 claimed proof was retracted after Paata Ivanishvili found a flaw (Aaronson’s blog). PSI’s X announcement had ~727k views on Nov 7
Show 1 more
- No reaction from Scott Aaronson or Andris Ambainis found on Nov 7 (Aaronson’s blog’s newest post, Nov 5, is on other topics)
What happened
Physical Superintelligence PBC posted the announcement, a paper PDF and Lean files on 6 Nov 2026. It says a run of its in-house system using a non-public Anthropic model produced a complete proof on day three, and Lean accepted both that proof and the final, improved version. The proof follows a strategy of Lovett and Zhang and proves an inequality they had left as a conjecture.
Why it matters
The conjecture is the main missing step for showing that quantum computers can’t get more than a polynomial speedup on unstructured problems for most inputs. Lean acceptance checks the formal statement as written. Whether the formal statement matches the conjecture is what the Stanford readers and other experts are now checking. This is also the first major result credited to a non-public Anthropic model.
What is disputed or not yet verified
| Verification | Lean-checked (per PSI, repository public); read by four Stanford theorists; unrefereed |
|---|
Reactions
Reaction from the conjecture’s co-author
On 8 Nov Scott Aaronson wrote5 that he believes the proof is correct for two reasons: “there’s a Lean certificate” and human experts “have already gone over it and understood it”. He said he had not yet understood the proof himself, that it is unclear what PSI’s harness added beyond the internal Claude model, and that the result rules out only one narrow kind of quantum speed-up (yes/no problems relative to random oracles), not Shor’s algorithm or quantum simulation.
Sources
7 sources from 5 sites. Numbers match the chips in the text.
7 sources: 4 primary, 3 reactions
Primary
- PSI: Aaronson–Ambainis conjecture (announcement)psi.inc, official
- Paper and Lean proofs (GitHub)github.com, code
- PSI on X (thread, ~727k views)x.com, official
- Aaronson & Ambainis, The Need for Structure in Quantum Speedups (arXiv 0911.0996)arxiv.org, paper
Reactions
- Scott Aaronson: Aaronson-Ambainis Conjecture proved! (By AI, of course) (8 Nov)scottaaronson.blog, discussion
- Comment on Aaronson’s 2019 post asking about the PSI proof (6 Nov)scottaaronson.blog, discussion
- Scott Aaronson: The Aaronson-Ambainis Conjecture (2008-2019), on the retracted 2019 attemptscottaaronson.blog, discussion
Changes
- Added Aaronson’s 8 Nov blog post
- Re-checked reactions (web search): none from Aaronson or Ambainis yet
- Filed (Techmeme and PSI X thread)