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