The Classification of Finite Simple Groups (CFSG), one of the most complex and sprawling theorems in mathematics, has been fully formalized in the Lean proof assistant. This milestone represents a landmark achievement in formalized mathematics, verifying thousands of pages of proof across dozens of papers.
Background
The Classification of Finite Simple Groups, completed in the 1980s, spans thousands of pages across hundreds of papers by dozens of mathematicians. Its formalization in Lean, led by Georg Gohr and collaborators, demonstrates the feasibility of verifying landmark results in group theory using interactive theorem provers.
- Source
- Hacker News (RSS)
- Published
- Oct 28, 2026 at 12:29 AM
- Score
- 8.0 / 10