Lean formally verifies the classification of finite simple groups

Classification of Finite Simple Groups Formalized in Lean

A team has completed a Lean formalization of the first-generation proof of the classification of finite simple groups, a result spanning thousands of journal pages and decades of work by roughly a hundred mathematicians. The project comprises 43.1 million lines of Lean, 2.05 million declarations, and 715 cited papers and books. During the effort, the team uncovered an issue in a published argument for the Unbalanced Group Theorem and developed an alternative route, detailed in an accompanying paper.