AI System Claims Proof of 18-Year-Old Quantum Conjecture, Verified in Lean

winer666 · reddit · 2026-11-08

Physical Superintelligence (PSI) announced Nov 6 that an internal research system running instances of a non-public Anthropic model produced a complete proof of the Aaronson–Ambainis conjecture — open since 2008, concerning whether quantum computers can be exponentially faster on unstructured problems — on day three of a run.
The proof was accepted by the Lean proof assistant: the formalization contains 648 machine-checked theorems with no placeholders or added axioms, replayed through Lean's kernel and the independent checker lean4lean. The system then improved the result twice, each version re-checked. Paper and Lean 4 formalization are public.
Caveats: humans must still confirm the formal statement matches the original conjecture; the prose paper isn't machine-checked; the model is non-public so the three-day run can't be reproduced — only the proof is verifiable.
If it holds up, this is AI doing real mathematics rather than assisting — raising the question of what happens to mathematics when discovery can't be inspected and only the final proof is checkable.

More from Models