Physical Superintelligence (PSI) announced on November 6 that an internal research system running instances of a non-public Anthropic model produced a complete proof of the Aaronson-Ambainis conjecture, a quantum-computing question open since 2008. The system had a complete proof on the third day of its run on PSI's own infrastructure, and the Lean proof assistant accepted it; PSI then pointed the system at related problems and it improved the result twice before Lean accepted the final version.

PSI published both the human-readable paper and the Lean 4 formalization on GitHub. The formal development — hundreds of machine-checked theorems — contains no unproven placeholders or added axioms according to the repository's own audit, and its declarations were replayed through Lean's kernel and lean4lean, an independent type checker. David Turturean of PSI built and ran the research system, framed the problem and takes responsibility for the paper's correctness.

The caveats are explicit in PSI's own material. The paper is a preprint with no peer review yet, the prose paper is not itself machine-checked, and human experts still have to confirm that the formalized statement matches the conjecture Aaronson and Ambainis actually posed. PSI has not identified which Anthropic model it ran, and Anthropic has not commented.