The Pulse
Axiom Formalizes the 15,000-Page Classification of Finite Simple Groups
Axiom says its AI-agent teams helped produce a 43.1-million-line Lean formalization of the Classification of Finite Simple Groups in 24 days. The work also surfaced errors and gaps in published arguments, including a flaw in one route to th
AI.info Team · Written with AI · fact-checked ·
On October 26, Axiom announced that it had turned the Classification of Finite Simple Groups into a computer-checkable Lean proof, a project it says took 24 days and produced about 43.1 million lines of code. The theorem, known as CFSG, describes the basic building blocks of finite groups—a mathematical result whose original proof stretches across roughly 15,000 pages, more than 500 papers and the work of about 100 mathematicians.
A proof assembled from hundreds of papers
Finite groups describe systems of symmetries. CFSG says every finite simple group belongs to a defined list: cyclic groups of prime order, alternating groups, sixteen infinite families of groups of Lie type, or one of 26 sporadic groups. Establishing that the list is complete required generations of mathematicians to build and connect results scattered through a large body of literature.
Axiom’s announcement is about formalizing that established classification, not discovering the classification itself. The company says its engineers and mathematicians directed swarms of AI agents to translate the first-generation proof into Lean, a language in which a proof assistant can check each deduction. Its public project page reports 43.1 million lines of Lean, 2.05 million declarations and 715 source papers and books; the company says the formalization builds on prior Lean work, including roughly 1.2 million lines from the Qiuzhen-CFSG project.
Agents divided the work; people checked the target
Axiom opened a Slack channel to coordinate the project on October 1, then launched its first agent swarm on October 2. An internal proof map divided the effort into 108 milestones and about 380 smaller tasks. According to the company, lead agents broke down difficult arguments and reviewed the statements being formalized, while other agents searched for existing results or wrote Lean proofs; human mathematicians investigated mathematical obstacles as engineers maintained the shared system.
The initial plan did not hold throughout. Axiom says some tasks depended on prerequisites that agents had assumed rather than proved, prompting the team to discard tens of thousands of lines and restart parts of the work. Lean can check that a formal deduction follows from its assumptions, but the people overseeing a project still have to check that the formal statement and definitions express the intended theorem. Axiom says its reviewers inspected that specification while Lean checked the deductions.
A published route to the Unbalanced Group Theorem had a flaw
Formalizing the literature also exposed trouble in one published argument for the Unbalanced Group Theorem, a result used in a substantial part of the classification. Axiom says its agents found counterexamples to a closure assertion in John Walter’s 1986 treatment. The company explicitly says those counterexamples did not disprove the Unbalanced Group Theorem; they left a step in that particular route unjustified.
In a paper published October 27, Colin Defant and Ken Ono describe the scope of the issue: “This obstruction concerns that particular argument. UGT also has other proofs.” Colin Defant and Ken Ono, “The Unbalanced Group Theorem”
Axiom says group theorists Richard Lyons and Ronald Solomon advised on the problem, and that the alternative argument drew on Solomon’s 1976 work. AxiomProver produced and formalized a new result called “Preservation of simple tops” for this route. The accompanying paper also records a shorter deduction found by Axiom mathematicians after the formalization that reaches the needed conclusion without that new theorem.
The code is public; the errata list is still being compiled
Axiom has made the formalization available through a public GitHub repository and an interactive proof map. The repository describes the work as a “sorry-free” Lean 4 proof, built on Mathlib and TauCeti and using Lean’s standard axioms. That lets other researchers inspect the code and build the project, while the formal theorem’s exact statement remains part of what humans must assess.
The project also records 34 “noteworthy deviations” from the published record that Axiom says required resolution; many other reports concerned typos, table errors, omitted hypotheses or steps recoverable from context. The company says it is preparing a detailed errata list with group theorists, and its project page says the list is still being compiled. Axiom’s release therefore makes a substantial formal proof available for inspection, but the public account of the corrections is not yet complete.