Classification of Finite Simple Groups Formalized in Lean

A new group theory result that came out of this formalization project is reported in this paper. While formalizing the first-generation proof, we found counterexamples to a closure assertion used in a published route to the Unbalanced Group Theorem. The paper explains the obstruction and gives an alternative argument for the simple-group case, built on Solomon’s 1976 theory of maximal 2-components, whose key step is Theorem 2.3, the preservation of simple tops.