Overview
- Physical Superintelligence said on November 6 that a research system running an unreleased Anthropic model produced a proof of the Aaronson–Ambainis conjecture after about three days of runs.
- The proof and a Lean 4 formalization are public and Lean accepted the formalization, with PSI reporting two automated improvements before final acceptance.
- The conjecture, posed in 2008, concerns when quantum computers can get exponential speedups on random inputs and the claimed proof gives explicit bounds that restrict such speedups to special structured cases.
- Key open questions remain because the Anthropic model is private and machine checking does not by itself confirm that the formalized statements match the informal conjecture, so independent experts at Stanford and elsewhere are reviewing the formalization and the manuscript.
- The episode underscores that AI systems can rapidly produce machine-checked math but that reproducibility, transparency, credit and months of human peer review will decide whether this result becomes accepted knowledge.