Working largely autonomously over 11 days, Claude produced the first end-to-end, computer-verified proof of Fermat's Last Theorem in the Lean proof assistant, writing 13 million lines of Lean and proving 30,300 intermediate theorems (29,500…
In the News: September 4, 2026 (Evening)
Anthropic says Claude formalized Fermat's Last Theorem in Lean over 11 days, after a DAG of theorem dependencies fixed a multi-agent coordination failure.
Evening edition
Machine-readable
Download Markdown