On November 6, 2026, Physical Superintelligence (PSI) said its internal research system had produced a proof of the Aaronson–Ambainis conjecture using an unnamed, non-public Anthropic model. PSI said Lean accepted the formalization. Its public repository spells out the mathematical statement, while leaving readers to confirm that the formal version matches the intended conjecture. PSI’s announcement · PSI’s Lean repository
What PSI says its system proved
The Aaronson–Ambainis conjecture concerns the influence of individual input bits on bounded, low-degree polynomials, and its connection to how many input queries classical computers need to simulate certain quantum algorithms. PSI described the conjecture as open since 2008.
PSI said its system found a complete proof on the third day of its run, then improved the result twice before Lean accepted the final version. The company’s repository names a formal theorem aaronson_ambainis and states its conditions explicitly: a real polynomial in N variables, of degree at most d, must take values between 0 and 1 on the Boolean cube {0,1}^N, with variance of at least ε under uniformly random inputs. The repository’s formal statement
Under those conditions, the repository states that at least one coordinate has squared-flip influence of at least (8√15/(125π⁴)) · ε^(5/2)/d⁶, and at least (ε/d)^7. Squared-flip influence is the expected squared change in the polynomial’s value when one input bit is flipped, averaging over uniformly random inputs. The theorem’s claim is that some bit must have a measurable influence under this definition.
A machine-checked proof verifies a formal statement; deciding whether that statement captures the intended conjecture is a separate mathematical task.
What Lean checks, and where human judgment enters
Lean is a proof assistant: it checks that a formal proof follows from specified logical rules and definitions. PSI’s repository lists four final Lean theorem declarations and says the formal development has no placeholders or added axioms. It also reports replaying checks through Lean’s kernel and lean4lean, another Lean checker. These are descriptions of the repository’s formalization and checks. PSI’s repository
That verification applies to the propositions encoded in Lean. The repository calls its formal version PrintedConjecture, but says readers must confirm that this formal statement corresponds to the conjecture the authors intended. It also says the human-readable paper is not itself machine-checked. Lean’s kernel and compiler, Mathlib’s definitions, and the checking machines remain part of the system’s trust basis.
PSI said in its November 6 announcement that Stanford researchers Guy Blanc, Jordan Docter, Carmen Strassle and Li-Yang Tan were reading the proof, had sent comments and were preparing a shorter exposition for experts. That describes the review activity PSI reported on that date. PSI’s announcement
What the result means for quantum queries
PSI’s claimed consequence is about query complexity, or the number of times an algorithm reads parts of its input. PSI says that after T quantum queries, an algorithm’s probability of answering “yes” can be represented by a bounded polynomial of degree at most 2T.
The conjecture’s consequence, as PSI describes it, is that a classical algorithm can use polynomially many input reads to approximate that yes-probability on all but a small fraction of random inputs, for fixed error and fraction. This is a result about query counts under those conditions, not a general bound on total runtime for every quantum-computing task. PSI’s explanation of the implication
