Project claims complete Lean formalization of finite simple group classification

A mathematical formalization project says it has encoded the complete first-generation proof of the classification of finite simple groups in Lean, with every logical step checked by the software's kernel. The original proof spans thousands of journal pages and decades of work. During formalization, the team found counterexamples to a closure assertion in a published route to the Unbalanced Group Theorem. An accompanying 35-page paper describes the obstruction and an alternative argument for the simple-group case. The team is working with group theorists to compile further errata from the literature.