Did an AI just prove an 18-year-old quantum conjecture?

Physical Superintelligence, a research lab based in Cambridge, Massachusetts, announced on November 6 that a research system it built in-house found a proof of the Aaronson-Ambainis conjecture, open since 2008. The system ran instances of a non-public Anthropic model on PSI's own infrastructure, and had a complete proof during the third day of the run. Lean, a proof assistant in which a computer checks every step, accepted it. PSI then set the system on related open problems, and it improved the result twice — Lean accepted the final version too. PSI put it bluntly: "The Aaronson-Ambainis conjecture is now a theorem."

David Turturean, a member of PSI's technical staff, led the work: he built the research system, scoped the problem, ran it, prompted the model to turn the results into a first draft of the paper, reviewed the draft, and takes responsibility for its correctness. PSI says advisor Jim Halverson audited the proof and advisor Phiala Shanahan commented on the Lean formalization. The paper and the Lean code are public on GitHub, with the code under an Apache 2.0 license.

Scott Aaronson and Andris Ambainis asked when a quantum computer can be exponentially faster than an ordinary one. The famous quantum speedups all exploit structure: Peter Shor's 1994 factoring algorithm works because the problem hides a repeating pattern. But on a random input — a string of 0s and 1s with no pattern to exploit — nobody knew whether a quantum computer could still be exponentially faster.

Aaronson and Ambainis turned the question into pure mathematics about polynomials. A quantum computer's chance of answering "yes" can be written as a polynomial in the input bits, and they conjectured that for these polynomials, some input bit always has a large influence on the result — enough that an ordinary computer can find it, read it, and estimate the quantum answer without many more reads. PSI's proof gives that guarantee: for a bounded polynomial of degree at most d, some bit's influence is at least (ε/d)^7, where ε measures how much the polynomial's value varies. Earlier guarantees decayed exponentially as the degree grew; this one decays only as a power.

The proof follows a plan by Shachar Lovett and Jiapeng Zhang, replacing one inequality their plan left as a conjecture with a new inequality proved in the paper. The key step pairs up input settings one-to-one, with a determinant producing the pairing — a strengthening of David Reimer's Butterfly Lemma.

The checkable part is genuinely strong. The Lean development is complete: four theorems proved with no placeholder and no added axiom, re-checked by two independent implementations of the Lean kernel, according to the repository. The formal statement is a short definition called PrintedConjecture, written using only Mathlib, so any reader can compare it against the conjecture as printed in Aaronson and Ambainis's paper. The repository also records its checks and includes an axiom audit.

What Lean cannot check is whether that formal statement is the right one. The human-readable paper is not itself machine-checked, and confirming that PrintedConjecture matches the conjecture as Aaronson and Ambainis meant it is a job for human experts — one that has not happened yet. As of November 7, no outside specialist has published an independent assessment, and Aaronson has not publicly weighed in. The Stanford team that settled a special case of the conjecture in August — Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan — is reading the proof and writing a shorter exposition for experts; PSI quotes them calling it "a huge result" with a proof brought together "in a rather magical way," but that is PSI reporting their words, not an independent verdict. And the Anthropic model is non-public, so nobody outside PSI can repeat the three-day run.

If the proof survives expert review, quantum algorithm research gets a clearer map: exponential speedups need structure, and random inputs are off the table for yes-or-no questions. That points researchers toward problems with exploitable structure — the Shor-style cases — rather than hoping for speedups on unstructured data.

The result is narrower than it sounds, and the limits matter. It counts queries — how many times a computer must read its input — not total computing time, so a classical computer might need few reads but a lot of computation between them. It covers most random inputs, not every input, and it does not rule out moderate speedups on unstructured problems or dramatic gains on structured ones. What to watch now: the Stanford team's exposition, Aaronson's response, and whether independent mathematicians confirm that the formal statement matches the printed conjecture.