GoKawiilLean Formalization Completes Classification of Finite Simple Groups
A research team has produced a complete machine-checked formalization in the Lean proof assistant of the classification of finite simple groups, following the original first-generation proof. The formalization comprises over 43 million lines of Lean code and 2.05 million declarations, drawing on 715 papers and books. The team also reports finding an issue in a previously published argument for the Unbalanced Group Theorem and describes the alternative proof route they used instead.