Classification of Finite Simple Groups Formalized in Lean
Summary
The CFSG project formalizes the Classification of Finite Simple Groups within Lean, providing an interactive proof map, a public GitHub repository, and a corpus of linked papers. The page highlights substantial collaboration (hundreds of contributors) and notes findings such as an issue in a published approach to the Unbalanced Group Theorem, with a complete Lean-based verification of the first-generation proof. It also provides citations, a BibTeX entry, and references to related blog posts and papers.