Number theory · Sep 4, 2026
Fermat's Last Theorem — new formalization
A new AI-assisted end-to-end Lean development is reported in September, formalizing an already proved theorem.
Scope and what remains
Original theorem resolution is in the 1990s; the 2026 event is formalization, not discovery. Check the exact natural-number formulation and transitive assumptions.
Contributors
Tianyi Peng's directed Claude workflow; retain Wiles, Taylor–Wiles, Darmon–Diamond–Taylor exposition, the Imperial project and Mathlib contributors as mathematical/library predecessors.
AI systems: Claude