PSI claims AI proof of an 18-year quantum conjecture, releases verification code

Physical Superintelligence (PSI) said on November 6 that an internal AI research system had found a proof of the Aaronson–Ambainis conjecture, a quantum-complexity problem open since 2008. It released a paper and Lean 4 code, saying it used a non-public Anthropic model.

Researchers can compare the original conjecture with the encoded propositions and obtain code and records for reproducing the checks. The code and documentation use Apache 2.0; the paper remains under its author’s copyright. The release also states a review boundary: humans must assess whether the encoded statement matches the original problem.

The relevant measure is query complexity: how many times an algorithm reads its input. Aaronson and Ambainis showed that their conjecture would allow a classical algorithm to approximate a T-query quantum algorithm’s acceptance probability on most inputs using polynomially many queries in T. The approximation allows a fixed error and a fixed fraction of exceptional inputs. That concerns input access, rather than a comparison of total running time across all quantum applications.

The mathematical statement concerns low-degree polynomials whose values stay within a bounded range on strings of zeroes and ones. If the output has positive variance, at least one input bit must have a sufficiently large influence, measured by averaging the squared change when flipped. PSI’s statement document specifies a lower bound of the variance-to-degree ratio raised to the seventh power, independent of the number of bits, and links it to the formal definitions.

According to the paper’s AI disclosure, David Turturean scoped the problem and built PSI’s research harness. Model instances searched for existing ideas, proposed and tested approaches, and coordinated work. The appendix says a complete proof emerged on the third day; two subsequent improvements reduced an exponent from 22 to 11 and then 7. The improvements followed instructions to explore other open problems using the intermediate results. Turturean reviewed the model-generated manuscript and accepts responsibility for its correctness.

What the proof checks cover

The verification library contains 761 declarations across 84 modules, according to its axiom audit: 648 theorems and 113 definitions. It reports that the final theorems depend only on three standard Lean foundational axioms. The library contains no additional axiom or unfinished-proof placeholder. Three core results stand separately from a fourth, stronger bound that takes an external research result as a hypothesis. The audit says this hypothesis is absent from the other three theorems.

The verification notes distinguish scanning source text from replaying proof terms through a checker. The latter checks were performed with Lean and a separately implemented checker, including replays starting from an empty environment that covered the underlying libraries. Historical runs on October 22 are identified separately from publication-preparation checks.

The November 6 release-preparation record reports passing builds, axiom checks, a replay of 84 modules and comparison checks for four final theorems. Controls accepted one correct example and rejected four incorrect examples. These are PSI’s published execution artifacts: readers can inspect captured results even though the original staging-run links remain private.

A paper-to-code guide maps mathematical claims to Lean declarations. Some explanatory parts of the manuscript, including motivation, related work and discussions of consequences, have no formal counterpart. Machine checking establishes a derivation of the encoded propositions. The correspondence guide identifies those boundaries, leaving the surrounding mathematical explanation for human review.

PSI says four Stanford researchers have read the proof, sent comments and are preparing a shorter exposition for specialists.