Axiom announces Lean formalization of finite simple groups classification

Axiom announced a Lean auto-formalization of the Classification of Finite Simple Groups on Oct. 27, calling it complete and computer-verified. @andrew_v10209 puts the release at over 43 million lines of Lean and cites 100 substantive fixes to the literature; @omarsar0 instead gives a roughly 50-million-line figure. Those posts do not independently establish the formalization’s completeness or the reported corrections.