Anthropic: Claude wrote a Lean proof of Fermat's Last Theorem in 11 days

Anthropic published a complete Lean 4 proof of Fermat's Last Theorem: 13 million lines, 29,500 intermediate theorems and about 6 billion output tokens, produced largely by Claude agents in 11 days. Mathematician Kevin Buzzard verified it but said the work tells us "essentially nothing" about mathematics.

• 13 million lines of Lean — over five times the size of the entire Mathlib library
• From-scratch build took 5 h 32 min on 96 jobs, peaking at 153 GB of RAM
• Independent Rust kernel nanoda checked 1,052,234 declarations with no errors
• List-price estimate for the tokens: about $300,000