# An AI system running an unreleased Anthropic model proved a quantum computing conjecture open since 2008

> Physical Superintelligence says its system found a Lean-checked proof of the Aaronson-Ambainis conjecture on day three of a run, then improved the bound twice.

- URL: https://devisdead.ai/news/an-ai-system-running-an-unreleased-anthropic-model-proved-a-quantum-computing-co
- Published: 2026-11-08T23:33:36Z
- Author: DevIsDead Newsroom
- Section: AI
- Tags: math, quantum computing, lean, anthropic
- Originally reported by Unite.AI (https://www.unite.ai/psi-reports-machine-checked-proof-of-aaronson-ambainis-conjecture/).

Another long-standing math problem has fallen to an AI. Physical Superintelligence (PSI) says an internal research system running a non-public Anthropic model proved the Aaronson-Ambainis conjecture, a problem that had stood since 2008, according to [Unite.AI](https://www.unite.ai/psi-reports-machine-checked-proof-of-aaronson-ambainis-conjecture/), whose article was written by an AI research agent and reviewed by its editors.

## What was proved

The question behind it: when do quantum computers get an exponential edge over classical machines? Shor's factoring algorithm wins because its input has a repeating structure to exploit. Aaronson-Ambainis concerns the opposite case: unstructured, random inputs. In 2008, Scott Aaronson and Andris Ambainis showed that if any low-degree polynomial bounded between 0 and 1 must have one input variable with a large influence, then any quantum algorithm with few queries can be simulated classically on most inputs with only polynomially more queries. In plain terms: on unstructured problems, no exponential quantum speedup. It doesn't rule out quantum advantage where there is structure.

## How it was done

According to PSI, a full proof came out on day three of a run on the company's own hardware, and Lean, the proof assistant, verified it. Given related open problems, the system then improved the result twice, with Lean accepting the final version. The proof builds on a strategy laid out by Jiapeng Zhang and Shachar Lovett, filling a gap in it with a new inequality. Both the paper and the Lean 4 code have been published.

The formal proof reportedly has no placeholders or added axioms, and was checked by Lean's kernel plus independent type checkers. The limits are stated plainly: a human still has to confirm the formal statement matches the conjecture as written, and the human-readable paper itself isn't machine-checked.

## Why it matters

This is the pattern to watch: AI search plus machine verification. The model can try ideas at scale; Lean decides which ones are actually true. It's the same combination behind [Axiom Math's verified library](/news/axiom-math-s-agents-turned-7-654-pages-of-human-math-into-16-million-lines-of-ch). The proof doesn't need anyone to trust the AI, only the checker.

**[Scoreboard](/scoreboard) update:** AI +1. An AI system settles a 2008 quantum computing conjecture with a machine-checked proof.

Stay undead.