Aaronson-Ambainis Conjecture Proved by PSI AI System
Physical Superintelligence says its AI proved the Aaronson-Ambainis conjecture, open since 2008; Lean accepted the machine-checked proof on day 3 of the run.
Hakkı ALKANPublished 3 min read
Physical Superintelligence (PSI) said on Nov. 6, 2026 that an internal AI research system, running a non-public Anthropic model, proved the Aaronson-Ambainis conjecture, a quantum complexity question open since 2008, according to the company's research announcement.
PSI says Lean, a proof assistant that machine-checks every step, accepted a complete proof on the third day of the run. The company later improved the result twice and published a paper plus a public Lean formalization. Outside peer review is still pending; treat this as a company claim with a checkable artifact, not a journal verdict.
What Is the Aaronson-Ambainis Conjecture?
Scott Aaronson and Andris Ambainis asked when quantum computers can be exponentially faster than classical ones. Speedups such as Shor's factoring lean on rare structure in the input. The conjecture, now claimed as a theorem, implies that on random yes-or-no inputs without that structure, quantum advantage is at most polynomial in the number of looks at the bits, not exponential.
Influence, here, means how much flipping one input bit moves a bounded low-degree polynomial that models a quantum algorithm's acceptance probability after a fixed number of queries.
How Did PSI's AI System Reach a Proof?
PSI says David Turturean, a member of technical staff, led the work: he built the research system, scoped the problem, ran it on company infrastructure, prompted a first paper draft, and remains responsible for correctness. Advisor Jim Halverson audited the proof; advisor Phiala Shanahan commented on the Lean formalization.
The run used instances of a non-public Anthropic model, beside other Anthropic capacity stories such as METR's Anthropic acceleration findings.
PSI posted the Lean sources in a public GitHub repository so outsiders can re-check the formalization, not only read the prose paper.
What Have Outside Researchers Said So Far?
In August 2026, Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle, and Li-Yang Tan proved there is no exponential speedup on random inputs for quantum algorithms that query in a fixed number of parallel rounds. PSI says that group has been reading the full proof, sent comments, and is writing a shorter expert exposition.
Via PSI's page, they wrote: "This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups."
For broader AI research-system context, see our note on GPT-6 cyber research claims.
Related Anthropic business context sits in our Anthropic IPO valuation coverage.
Our Take
A Lean-accepted formalization is a high bar for show-your-work, but journals and independent reproductions still matter. Watch whether the Stanford exposition lands cleanly, whether rival groups find gaps, and how often similar AI runs clear open problems with public checkers rather than press decks.
| Item | Details |
|---|---|
| Announced | Nov. 6, 2026 |
| Company | Physical Superintelligence (PSI) |
| Problem | Aaronson-Ambainis conjecture (open since 2008) |
| Model used | Non-public Anthropic model (per PSI) |
| Checker | Lean accepted proof on day 3; later improved twice |
| Artifacts | Paper + public GitHub Lean formalization |
| Status | Company claim; peer review pending |