Axiom Math releases a computer-checked proof of the classification of finite simple groups

Axiom Math published what it describes as the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG), written in the Lean proof assistant. The classification says every finite simple group is a cyclic group of prime order, an alternating group, a group of Lie type or one of the sporadic groups. Axiom’s post, headed “Formalizing the Enormous Theorem,” reports that swarms of AI agents wrote about 43.1 million lines of Lean in 24 days, working through 108 milestones and about 380 smaller tasks.

The original proof, by Axiom’s count, runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians. Axiom formalised the “first generation” proof rather than the second-generation revision, which it says is still incomplete. The formal development incorporates about 1.2 million lines from an earlier project, Qiuzhen-CFSG, plus Mathlib.

Lean checks the logical deductions; whether the formal statements express the intended classification is a matter of human review, which Axiom says its team and an advisory board that includes Richard Lyons and Ronald Solomon carried out. The post lists 34 noteworthy deviations from the published literature, most of them minor, such as typos, table errors and dropped hypotheses. It describes two substantive cases: a lemma in the Aschbacher–Smith treatment of the quasithin case where agents found a counterexample and the equality had to be replaced with an inequality, and a closure assertion in Walter’s argument for the Unbalanced Group Theorem, where counterexamples left a key inference unjustified. Axiom says its prover, AxiomProver, proved a new result (Theorem 2.3) to repair the second, and that its mathematicians later found a shorter route that avoids it. A full errata list is published on a separate site and Axiom says that curation is continuing.

These are Axiom’s own claims. The post credits the classification itself to the many mathematicians who built it and describes Axiom’s contribution as making the proof mechanically checkable; this entry found no independent reaction from group theorists in the sources opened. Because the formalisation covers one version of the proof, it does not settle the status of the second-generation proof.

The release arrived in the same week as OpenAI’s and Anthropic’s competing Exponential Time Hypothesis claims, and fits a pattern in which AI-assisted mathematics is increasingly presented with a Lean artefact rather than a prose argument alone.