Anthropic has formalized a complete proof of Fermat's Last Theorem (FLT) in Lean using their internal model on the prove2.me platform, becoming the final theorem to be formalized from Freek Wiedijk's famous list of 100 formalization challenges, which has been a 20-year benchmark. The proof, based on the Darmon-Diamond-Taylor exposition of the Wiles-Taylor-Wiles argument, consists of over 13.4 million lines of code and develops Fontaine theory and Mazur's work on the Eisenstein ideal. This achievement wraps up two decades of effort in formalized mathematics.
Background
Freek Wiedijk's list of 100 formalization challenges has been a benchmark in the formal mathematics community since the early 2000s, with Fermat's Last Theorem being one of the most difficult remaining problems. The Xena Project has been working on formalizing FLT in Lean as part of its educational mission to teach Lean through mathematical practice.
- Source
- Lobsters
- Published
- Sep 5, 2026 at 03:11 AM
- Score
- 9.0 / 10