---
id: "2026-11-06-psi-aaronson-ambainis-conjecture-proof"
url: "https://postcutoff.com/e/2026-11-06-psi-aaronson-ambainis-conjecture-proof/"
as_of: "2026-11-09T21:13:00+01:00"
date: "2026-11-06"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Lean-verified
sources: 7
editor: human editor
human_review: null
version: "2026-11-09"
---

As of: 2026-11-09 21:13 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-11-06-psi-aaronson-ambainis-conjecture-proof/

# PSI claims Lean-checked proof of the Aaronson–Ambainis conjecture

Full title: Physical Superintelligence says its system, running a non-public Anthropic model, proved the Aaronson–Ambainis conjecture (open since 2008), with a Lean check

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. The proof was found in a three-day run of PSI's research system using instances of a non-public Anthropic model, and Lean accepted it. Stanford theorists who read it call it "a huge result"; the paper is not yet refereed.

## 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/ ?'); 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
- 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 [wrote](https://scottaaronson.blog/?p=10295) 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.

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 190 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 129 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 220 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 159 days after its cutoff

## Sources

1. [PSI: Aaronson–Ambainis conjecture (announcement)](https://psi.inc/research/aaronson-ambainis/) (psi.inc, official)
2. [Paper and Lean proofs (GitHub)](https://github.com/physical-superintelligence/aaronson-ambainis) (github.com, code)
3. [PSI on X (thread, ~727k views)](https://x.com/psipbc/status/2118706269506949152) (x.com, official)
4. [Aaronson & Ambainis, The Need for Structure in Quantum Speedups (arXiv 0911.0996)](https://arxiv.org/abs/0911.0996) (arxiv.org, paper)
5. [Scott Aaronson: Aaronson-Ambainis Conjecture proved! (By AI, of course) (8 Nov)](https://scottaaronson.blog/?p=10295) (scottaaronson.blog, discussion)
6. [Comment on Aaronson's 2019 post asking about the PSI proof (6 Nov)](https://scottaaronson.blog/?p=4414#comment-2043129) (scottaaronson.blog, discussion)
7. [Scott Aaronson: The Aaronson-Ambainis Conjecture (2008-2019), on the retracted 2019 attempt](https://scottaaronson.blog/?p=4414) (scottaaronson.blog, discussion)

## Changes

- 2026-11-09: Added Aaronson's 8 Nov blog post
- 2026-11-08: Re-checked reactions (web search): none from Aaronson or Ambainis yet
- 2026-11-07 (filed): Created (Techmeme and PSI X thread)

## Related

- People: [Scott Aaronson](https://postcutoff.com/person/scott-aaronson/)
- Archived: 1 post, listed in https://postcutoff.com/e/2026-11-06-psi-aaronson-ambainis-conjecture-proof/index.json