PSI says its AI proved a 2008 quantum conjecture

An AI system says it has proved a theorem researchers have chased since 2008, and it shipped the proof in a form a computer can check.

That is the claim from PSI, which posted the result on Nov. 6. PSI says its internal research system, running instances of a non-public Anthropic model, found a proof of the Aaronson-Ambainis conjecture, and that the Lean proof assistant accepted it.

What PSI says it proved

The conjecture is about how much faster quantum computers can be. Aaronson and Ambainis posed it as a statement about polynomials. PSI's post explains that if it holds, quantum computers are at most polynomially faster than ordinary computers on random inputs, rather than exponentially faster.

PSI's main result: a bounded, non-constant polynomial of degree d with variance v has some bit whose influence is at least c times v to the power 5/2, divided by d to the sixth, with c about 0.0025. The post says it builds on work by Lovett and Zhang and by Reimer.

According to PSI, a complete proof appeared on day three of the run, and the system then improved the result twice. David Turturean of PSI led the work and is responsible for the paper's correctness, the post says. Advisor Jim Halverson audited the proof.

The checker is the story

Yes, AI breakthrough claims arrive every week. This one ships with its own receipt.

PSI's code repository holds a Lean 4 formalization next to the paper, under the Apache 2.0 license, with instructions to rerun the check on your own machine. The README says the mathematical statements, the paper's first draft and the Lean formalization were produced by AI models in a research harness Turturean built. It reports that the final theorems depend only on Lean's standard axioms.

That is what formal verification buys you. You do not have to trust the lab, the model or the press release. You run the checker.

The README states the limits itself. The paper is not machine-checked, and some passages have no Lean counterpart. One of the four public theorems takes as a hypothesis a result by Agarwal and Ben-David that has not been formalized. Neither PSI's post nor the README says the work has been peer reviewed.

Outside mathematicians are reading it. Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford, who proved a special case in August, have read the proof and sent comments, PSI says. Their verdict, as PSI quotes it: "This is a huge result."

What it means for you

You cannot use this model. Anthropic has not released it, and PSI does not name it.

What you can use is the pattern. AI-generated work is starting to arrive with a check attached. If a vendor tells you its agent wrote correct code or a sound analysis, ask what you can rerun to confirm it. Tests, proofs, reproducible evals. Anything less is a promise.

It also lands days after Anthropic's filing said the company may imminently cross its own AI R&D threshold. A research harness running an unreleased model and settling an open problem is the kind of result that threshold is about.

What to watch

The Stanford group's comments, and whether a journal referee signs off on the parts of the paper Lean does not cover. Then whether Anthropic says which model did the work.

Rerun the proof. Then wait for the referees.