Classification of Finite Simple Groups Formalized in Lean

A large collaborative project has completed a Lean formalization of the first-generation proof of the classification of finite simple groups. The theorem says that every finite simple group belongs to one of four categories: cyclic groups of prime order, alternating groups, groups of Lie type, or one of 26 sporadic groups. The original proof accumulated across thousands of pages, roughly a hundred mathematicians, and several decades; this formalization encodes its logical steps so Lean’s kernel can check them. The project reports 43.1 million lines of Lean, 2.05 million declarations, and 100 milestones, drawing on 715 papers and books. Its site provides a proof map and links to the formalization and project materials.

The work also led to a new result concerning the Unbalanced Group Theorem. During formalization, the team found counterexamples to a closure assertion in a published argument used on one route to that theorem. Their accompanying paper describes the problem and supplies an alternative proof for the simple-group case, based on Solomon’s 1976 theory of maximal 2-components. A central step is showing that simple tops are preserved. The project presents formalization not only as a way to verify an extensive proof, but also as a means of checking established mathematical arguments closely enough to expose errors and develop a replacement. Its interactive resources trace the proof’s milestones, source works, and Lean implementation.