PSI’s AI System Produces a Lean-Checked Proof of the Aaronson-Ambainis Conjecture

A conjecture that has shaped arguments about quantum speedups since 2008 now has a machine-checked proof, Physical Superintelligence said Friday. The physics research lab reported that an internal research system, running instances of a non-public Anthropic model on PSI’s own infrastructure, produced a complete proof of the Aaronson-Ambainis conjecture on the third day of a run, and that the Lean proof assistant accepted it.

In a research post, PSI put the claim bluntly: “The Aaronson-Ambainis conjecture is now a theorem.” Scott Aaronson and Andris Ambainis linked the question to polynomials and argued that, if their conjecture held, quantum computers would have at most a polynomial advantage in the number of input queries needed for yes-or-no questions on random inputs that lack rare structure. Dramatic speedups such as Shor’s factoring algorithm still depend on promised patterns in the input, PSI wrote, summarizing that longer-running debate.

What the system produced

David Turturean, a member of technical staff at PSI, led the work: he built the research system, scoped the problem, ran it, then prompted the model to turn the output into a first draft of the paper, which he reviewed and for which he is responsible. After Lean accepted the day-three proof, PSI said it pointed the system at related open problems. The system improved the result twice, and Lean accepted the final version. Advisor Jim Halverson audited the proof, and advisor Phiala Shanahan commented on the Lean formalization, according to the post.

The manuscript and a Lean 4 formalization are public. The Lean code, scripts and documentation are released under Apache 2.0; the paper remains copyright of its author. The repository lists four theorems proved with no placeholders or added axioms, and says they were re-checked with two independent Lean kernel implementations. It also leaves an important job to readers: confirming that the formal statement labeled PrintedConjecture matches the conjecture as printed. The human-readable paper is not itself machine-checked. Business Insider’s Kelsey Vlamis reported that Anthropic did not respond to a request for comment on which unreleased model was used.

Limits the proof is meant to settle

PSI’s write-up walks through the influence bound the team says it proved for bounded, low-degree polynomials on the discrete cube, including an explicit constant of about 0.0025 in one form of the inequality. With the conjecture in hand, the lab says an ordinary computer can estimate a quantum algorithm’s acceptance probability, up to a small error, for all but a small fraction of random strings, using a number of looks that grows like a fixed power of the quantum look count rather than exponentially. That still leaves structured problems, Shor’s algorithm among them, outside that “random input” story.

In August, Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan of Stanford had proved there is no exponential speedup on random inputs for quantum algorithms that read their input in a fixed number of parallel rounds. PSI says the same group has been reading the full-conjecture proof and is writing a shorter exposition for experts. Relayed through PSI’s post, they wrote: “This is a huge result.” They added: “Everything is brought together in a rather magical way.”

PSI closed its announcement: “Quantum computing still has plenty of mysteries, but now there is one fewer.”