Fermat's Last Theorem in Lean 4

Anthropic has released a complete, machine-checked proof of Fermat's Last Theorem formalized in Lean 4, based on the mathematical arguments of Frey, Serre, Ribet, Wiles, and Taylor-Wiles. The proof was verified through a full build of over 60,000 modules and confirmed by an independent Rust-based kernel (nanoda), relying only on Lean's three standard axioms with no gaps or additional assumptions. This represents a significant milestone in formal mathematics, as one of history's most famous theorems has now been rigorously verified by a computer.