Anthropic reports that Claude autonomously produced the first complete computer-checked proof of Fermat's Last Theorem in 11 days, writing 13 million lines of Lean code and proving 29,500 intermediate theorems. The result represents a major milestone for AI-assisted formal mathematics and was reviewed by mathematician Kevin Buzzard.
Background
Fermat's Last Theorem, conjectured in 1637 and proved by Andrew Wiles in 1995, has long been a benchmark for mathematical verification. The Lean proof assistant community has been working on formalizing Wiles's proof since 2024.
- Source
- Lobsters
- Published
- Sep 5, 2026 at 08:54 PM
- Score
- 8.0 / 10