PSI Reports Machine-Checked Proof of Aaronson-Ambainis Conjecture

Physical Superintelligence announced on November 6, 2026 that an internal research system running instances of a non-public Anthropic model had found a proof of the Aaronson-Ambainis conjecture, a quantum-computing problem open since 2008.

The system produced a complete proof during the third day of a run on PSI’s own infrastructure, and the Lean proof assistant accepted it. PSI then assigned related open problems to the system, which improved the result twice before Lean accepted the final version. The manuscript and Lean 4 formalization are public.

What the Conjecture Says About Quantum Speedups

The question concerns when quantum computers can be exponentially faster than classical machines. Shor’s 1994 factoring algorithm depends on structure: its input carries a repeating pattern that the algorithm can exploit. PSI’s result addresses the contrasting case of random or unstructured inputs, where such a pattern is generally absent.

In the query model, a classical algorithm reads one bit per query, while a quantum query can be spread in superposition across many input positions. PSI’s explanation connects this model 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 therefore 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 polynomially many queries in T. 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.

Formally, the repository considers 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 ε, some coordinate has an influence of at least (8√15 / (125π⁴)) · ε^(5/2) / d⁶, and consequently at least (ε/d)⁷. Influence is the expected squared change in p when that coordinate’s bit is flipped.

How the Proof Was Built and Checked

The argument follows a plan by Shachar Lovett and Jiapeng Zhang based on fractional certificates and level sets, but replaces an inequality their plan left conjectural with a new all-pairs inequality. 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 needed for the new inequality.

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, and establishing a row bound with a pointwise sensitivity bound. Together, those steps yield the explicit influence bound.

The formal development contains no proof placeholders or added axioms, according to the repository’s recorded audit. Its declarations were replayed through Lean’s kernel and 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, it accepted one correct small solution and rejected four deliberately wrong ones.

Those checks have explicit limits. A reader must still confirm that the formal statement matches the printed conjecture. The human-readable paper is not itself machine-checked, while Lean’s kernel and compiler, Mathlib’s definitions, and the machines used for checking remain part of the trusted base.

Human Roles and Expert Review

David Turturean, a member of PSI’s technical staff, developed and ran the research system, 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, first draft and Lean formalization. Jim Halverson audited the proof, and Phiala Shanahan commented on the formalization.

The announcement follows a paper submitted on August 19, 2026 by Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan. Those authors had 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.

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.”

The immediate test is unusually concrete: independent kernels can replay the encoded argument, while experts must still confirm that the encoded statement matches Aaronson and Ambainis’s conjecture and assess the parts of the paper outside Lean. That division determines what the machine checks establish and what still requires human mathematical review.