Axiom says AI agents formalized the enormous theorem in Lean in 24 days

Axiom Math says it has released the first complete computer-checked proof in Lean of the Classification of Finite Simple Groups (CFSG), often called the enormous theorem, which lists the building blocks of finite groups and originally spanned roughly 15,000 pages across hundreds of papers. Axiom reports that over 24 days its engineers and mathematicians directed swarms of AI agents that produced about 43.1 million lines of Lean, and that formalization found dozens of noteworthy deviations from the published record that needed fixing, including work around the Unbalanced Group Theorem. These are Axiom's claims; the release includes a repository others can inspect and an errata list for group theorists.