AI System Produces Machine-Checked Proof of 18-Year-Old Quantum Conjecture

Physical Superintelligence announced on November 6, 2026 that an internal research system running instances of a non-public Anthropic model has produced a proof of the Aaronson-Ambainis conjecture, a quantum-computing problem open since 2008. The Lean proof assistant accepted the complete formalization, and both the manuscript and the Lean 4 code are now public.

The system found the proof on the third day of a run on PSI's own infrastructure. PSI then gave it related open problems, the system improved the result twice, and Lean accepted the final version. That timeline matters. A proof of an 18-year-old conjecture, produced and machine-verified in days, is a data point in the debate over whether AI systems can do genuinely novel mathematics rather than recombine known results.

What does the conjecture actually say?

The question sits at the core of quantum computing's promise: when can quantum computers be exponentially faster than classical machines? Shor's 1994 factoring algorithm depends on structure — its input carries a repeating pattern the algorithm can exploit. The Aaronson-Ambainis conjecture addresses the opposite case: random or unstructured inputs, where such a pattern is generally absent.

The setting is the query model. A classical algorithm reads one bit per query. A quantum query can be spread in superposition across many input positions at once. PSI's explanation connects this to polynomials: after T quantum queries, the probability that the algorithm answers yes is a bounded polynomial of the input bits with degree at most 2T. Simulating the quantum algorithm then becomes a question of estimating that polynomial without reading exponentially many input bits.

In their original paper, Scott Aaronson and Andris Ambainis conjectured that every bounded low-degree polynomial has a highly influential variable. They proved that, assuming the conjecture, every T-query quantum algorithm can be simulated on most inputs by a classical algorithm making only polynomially many queries in T.

The stakes are about growth rates. The consequence is polynomial rather than exponential growth in classical queries for any fixed approximation error and fraction of excluded inputs. It does not rule out exponential quantum advantages for problems with suitable structure — it bounds the unstructured case.

What is the precise bound?

The repository works with a real polynomial p of degree at most d whose values on the discrete cube lie between 0 and 1. If its variance over a uniformly random input is at least ε, then some coordinate has an influence of at least (8√15 / (125π⁴)) · ε^(5/2) / d⁶, and consequently at least (ε/d)⁷.

Influence has a concrete definition here: the expected squared change in p when that coordinate's bit is flipped. The statement turns a vague intuition — "low-degree polynomials must depend strongly on some input" — into an explicit, checkable inequality.

How was the proof built and checked?

The argument follows a plan by Shachar Lovett and Jiapeng Zhang based on fractional certificates and level sets. But that plan left one inequality conjectural. PSI's proof replaces it with a new all-pairs inequality.

The mechanism is combinatorial. A determinant generates a one-to-one pairing of input settings. PSI says this pairing goes beyond David Reimer's weaker Butterfly Lemma pairing because it also limits how often paired settings agree on each coordinate — a bound the new inequality needs.

The repository divides the elementary proof into four parts:

• Deriving the all-pairs inequality from the determinant and bijection
• Integrating it over level sets
• Averaging over coordinates
• Establishing a row bound with a pointwise sensitivity bound

Together, those steps yield the explicit influence bound.

The formal development contains no proof placeholders and no added axioms, according to the repository's recorded audit. The declarations were replayed through Lean's kernel and through lean4lean, an independent implementation of Lean's type checker. In a sandboxed run, a comparator using the nanoda and Lean kernels accepted the four final theorems. On a second machine, the same comparator accepted one correct small solution and rejected four deliberately wrong ones.

That last test is worth pausing on. The team deliberately fed the checker broken mathematics to confirm it would catch errors, not just rubber-stamp whatever arrived.

What still rests on human trust?

The checks have explicit limits, and PSI discloses them. A reader must still confirm that the formal statement matches the printed conjecture. The human-readable paper is not itself machine-checked. And the trusted base — the parts that must be correct for the verification to mean anything — still includes Lean's kernel and compiler, Mathlib's definitions, and the machines used for checking.

In other words, Lean certifies the chain from axioms to theorem. It cannot certify that the theorem encoded in Lean is the theorem Aaronson and Ambainis wrote down in 2008. That judgment stays with human mathematicians.

Who did what?

David Turturean, a member of PSI's technical staff, developed and ran the research system. He scoped the problem, prompted the model to package a first draft, reviewed that draft, and is responsible for the paper's correctness. The repository discloses that AI models produced the mathematical statements, the first draft, and the Lean formalization. Jim Halverson audited the proof, and Phiala Shanahan commented on the formalization.

The division of labor is the story: the machine generated and formalized the mathematics, while a human scoped the problem, checked the output, and carries formal responsibility for correctness.

How does this connect to other recent work?

The announcement follows a paper submitted on August 19, 2026 by Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan. Those authors settled the classical-simulation consequence for parallel quantum algorithms, proving that a t-query, d-round algorithm can be simulated on most inputs with t^(O(d²)) classical queries.

PSI says all four have been reading the full proof, have supplied comments, and are preparing a shorter exposition for experts. Their engagement signals that specialists in the field are taking the result seriously enough to invest their own time in it.

In their assessment published by PSI, the researchers wrote: "This is a huge result. It resolves a decades-old conjecture with important implications for the nature of problems that admit quantum speedups. The proof draws on and extends several lines of work in the analysis of boolean functions and probabilistic combinatorics. Everything is brought together in a rather magical way."

What happens next?

The immediate test is unusually concrete. Independent kernels can replay the encoded argument, and they already have. But experts must still confirm that the encoded statement matches Aaronson and Ambainis's conjecture, and they must assess the parts of the paper that live outside Lean. That split — machine-checked derivation, human-checked correspondence — now defines what this kind of AI-assisted proof establishes and what it cannot.