Axiom reports a 24-day Lean formalization of CFSG
Axiom Math says that dozens of AI agents, coordinated with human mathematicians and engineers, completed a Lean formalization of the first-generation proof of the Classification of Finite Simple Groups in 24 days. The company reports about 43.1 million lines of Lean code and 2.05 million declarations, and has opened the repository for inspection. Axiom also says the formalization uncovered an issue in a published argument for the Unbalanced Group Theorem, leading to an alternative route and the result “Preservation of simple tops.” The repository’s review status is described as a team assessment; external mathematicians still need to verify that the formal statement matches CFSG and independently assess the claimed issue and repair.
The project organizes a vast proof distributed across hundreds of publications into a machine-checkable dependency graph that researchers can rerun, inspect, maintain and potentially reuse. It also demonstrates multi-agent systems being applied to the coordinated engineering required for large-scale formal mathematics, while its mathematical claims remain subject to external review.
The classification of finite simple groups is one of the great collective achievements of mathematics. Its first-generation proof spans thousands of journal pages, written by about a hundred mathematicians over several decades. It shows that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups.
Here we present a complete formalization in Lean following the first-generation proof, with every logical step checked by Lean’s kernel. Along the way, we found an issue in a published argument for the Unbalanced Group Theorem. The accompanying paper explains the issue and the alternative route used in our proof. Our blog post tells the full story.
Lines of Lean 43.1M
Declarations 2.05M
Milestones 100
Papers and books 715
#Axiom Math#AxiomProver#Lean#Classification of Finite Simple Groups#Preservation of simple tops#Unbalanced Group Theorem#Mathlib#Qiuzhen-CFSG#TauCeti