Axiom Math Releases 43.1M-Line Lean Proof of Group Classification

Axiom Math said on October 27, 2026 that it is releasing what it calls the first complete computer-checked proof of the Classification of Finite Simple Groups, produced over 24 days by engineers and mathematicians directing swarms of dozens of AI agents that wrote approximately 43.1 million lines of code in the Lean proof assistant.

“Today, we are releasing the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG),” the company wrote in its announcement. The classification identifies the basic building blocks of finite groups, and its original proof extends across roughly 15,000 pages in more than 500 articles by about 100 mathematicians, a scale that earned it the nickname the enormous theorem.

What Axiom Released

CFSG establishes that every finite simple group is cyclic of prime order, alternating on at least five symbols, one of sixteen infinite families of groups of Lie type constructed over finite fields, or one of exactly 26 isolated sporadic groups; the announcement notes that some authors count the Tits group as a 27th. The largest sporadic group, the Monster, was constructed by Robert Griess in 1980 using an algebra of dimension 196,884.

The human proof effort stretched across decades. In 1963, Walter Feit and John Thompson proved that every nonabelian finite simple group has even order, in a 255-page paper that filled an entire issue of the Pacific Journal of Mathematics. Daniel Gorenstein laid out a sixteen-step program to finish the classification in 1972 and declared it complete in 1983, but the quasithin case rested on an unfinished manuscript by Geoffrey Mason until Michael Aschbacher and Stephen Smith published a 1,221-page treatment in 2004, closing what became known as the first-generation proof. A more systematic second-generation proof begun by Gorenstein and Richard Lyons, later joined by Ronald Solomon and Inna Capdeboscq, remains incomplete, so Axiom formalized the first-generation proof.

The project page presents the formalization as following the first-generation proof with every logical step checked by Lean’s kernel, and lists 43.1 million lines of Lean, 2.05 million declarations, and 715 papers and books in its corpus. Axiom says its proof map drew on the second-generation volumes, and that the formalization incorporates roughly 1.2 million lines of code from the earlier Qiuzhen-CFSG project and builds on Mathlib, which it credits to hundreds of contributors. The project names Dean Cureton, Vasily Ilin, Bhavik Mehta, and Niels Voss as core contributors, with Letong Hong as principal investigator.

The public GitHub repository describes the result as a sorry-free Lean4 proof, pinned to version 4.35.0-rc3, built on Mathlib and the TauCeti project and using only the standard axioms Classical.choice, propext, and Quot.sound, with no native_decide. Its formal statement of the classification, taken from TauCeti, reads: “Every finite simple group is isomorphic to one of the explicitly constructed groups on the classification list.” The README says lake build checks the entire development, and that open changes to the Lake build tool and optimizations the team plans to upstream brought build time under 24 hours; the code carries an Apache-2.0 license.

A 24-Day Swarm Effort

On October 1, 2026, Axiom opened a Slack channel to coordinate the project. Pre-existing Lean work and an internal proof map assembled from the published literature divided the effort into 108 milestones and about 380 smaller tasks; the first swarm went live on October 2, 2026, with agents claiming milestones through GitHub issues and reporting completed work in Slack. Lead agents decomposed difficult arguments and reviewed statements, while other agents searched for existing results or wrote Lean proofs, and an agent could delegate missing prerequisites to other agents whose results entered a shared repository.

Early progress exposed weak points. Some apparently manageable milestones concealed enormous prerequisites that agents had assumed rather than proved, and the team deleted tens of thousands of lines built on those assumptions before restarting on a sounder plan; one early milestone concerned the signalizer functor theorem, whose candidate proof relied on structural assumptions that still needed justification. Build times also became a bottleneck as agents produced proofs faster than Lean could recheck them. Axiom says its engineers distributed cached build results across workers, ran independent checks in parallel, and externalized expensive finite calculations into separately checkable certificates, changes the company says sped verification by orders of magnitude.

On October 10, 2026, a message in the channel announced that the agents had proved the Monster simple, the company recounts; the agents also formalized the Monster’s existence through the Griess algebra and a theorem identifying groups of Monster type with the Monster. On October 13, 2026, only one milestone closed, and engineers organized a replanning effort that split unfinished milestones into smaller, precisely stated theorems, each decomposition required to show how the pieces would establish the original milestone through a short Lean proof.

Gaps Found in the Published Proof

Translating the proof into Lean exposed problems in the published arguments, Axiom reports. Most were minor — typographical errors, errors in tables, or dropped hypotheses — but the company counts 34 noteworthy deviations from the published record, the most substantial relating to the Unbalanced Group Theorem, or UGT.

One example came from Aschbacher and Smith’s quasithin volumes, where a lemma asserted that two numerical quantities were equal. The agents found a counterexample involving the group SL₂(5), in which one quantity was 1 where the asserted equality required 2. Replacing the equality with an inequality corrected the lemma, but later arguments had used equality to rule out cases, so the team broadened an earlier argument to cover those configurations.

UGT helps identify a whole group from information about its subgroups: according to the abstract of the accompanying paper, under the classification’s inductive hypotheses, a nontrivial odd-order subgroup normal in the centralizer of an involution forces the ambient simple group to be of Lie type in odd characteristic or alternating of certain degrees. Axiom approached UGT through John Walter’s 1986 memoir, and while formalizing that argument its agents found explicit counterexamples to a closure assertion it used: an operation assumed to keep the associated simple groups within a specified family could produce a group explicitly excluded from it.

In the company’s account, starting from PSL₂(49), whose field involution has centralizer PGL₂(7), the operation yields the simple component PSL₂(7), which is excluded from the family because 7 is a Mersenne prime. Axiom notes the counterexamples did not refute UGT itself, or even the conclusion of Walter’s Proposition II.5.9(ii).

The repair drew on Solomon’s 1976 theory of maximal 2-components, which Axiom says supplied the central ideas for an alternative argument its AxiomProver system produced and formalized. The key step, stated in the paper as Theorem 2.3 (preservation of simple tops), is described by Axiom as a new result in group theory proved by AxiomProver; combined with the reductions of Gilman and Solomon and the recognition theorems of Foote and Harris, it supplies the simple-group form of UGT needed for the classification. After the formalization, Axiom mathematicians found a shorter deduction within first-generation methods, recorded as Remark 9.5, that reaches the same conclusion without Theorem 2.3.

That paper, The Unbalanced Group Theorem, contributed by Colin Defant and Ken Ono, appeared on the Hexagon preprint server as version 1 on October 27, 2026 under a CC BY 4.0 license; the project page lists it at 35 pages. Axiom says it is working with group theorists to compile the errata found in the literature and will publish them on the project’s errata page. Lyons and Solomon, whose work underpins the classification, were consulted on the UGT repair, and the company says it will keep curating and resolving the errata with an advisory board that includes them, alongside external advisor Dan Nakano. Axiom frames its contribution as making the proof mechanically checkable, documenting the obstructions encountered, and supplying formalized arguments that resolve them, while stating that the classification remains the achievement of the mathematicians who discovered the groups and developed the arguments.