Classification of Finite Simple Groups Formalized in Lean

Researchers have completed a full formalization of the Classification of Finite Simple Groups in the Lean proof assistant, with every logical step verified by Lean's kernel. During this formalization project, they discovered a flaw in a published proof of the Unbalanced Group Theorem and developed an alternative argument using Solomon's 1976 theory of maximal 2-components. The formalization spans 43.1 million lines of Lean code and represents a major effort to verify one of mathematics' most significant collective achievements.