Axiom Math: AI agents deliver first fully machine-checked proof of finite simple groups

What this is about

On October 27, 2026, Axiom Math published what it describes as the first complete, computer-verified proof of the classification of finite simple groups (CFSG). It took 24 days. Engineers and mathematicians directed swarms of dozens of AI agents, which wrote about 43.1 million lines of code in the Lean proof assistant. A proof assistant is a program that checks mathematical proofs step by step for logical correctness. All figures come from Axiom itself.

The classification describes the basic building blocks of finite groups. The original human proof runs to roughly 15,000 pages across more than 500 articles by about 100 mathematicians, which is why it is also called the "enormous theorem."

What the classification says

According to the CFSG, every finite simple group (a group that can't be broken down into smaller building blocks) is one of four things: cyclic of prime order, alternating on at least five symbols, a member of one of sixteen infinite families of Lie type over finite fields, or one of exactly 26 sporadic groups. Some authors count the Tits group as a 27th. Robert Griess constructed the largest sporadic group, the "Monster," in 1980 using an algebra of dimension 196,884.

The human proof took decades. In 1963, Walter Feit and John Thompson proved in 255 pages that every nonabelian finite simple group has even order. Daniel Gorenstein laid out a 16-step program in 1972 and declared the classification complete in 1983. However, the "quasithin" case relied on an unfinished manuscript by Geoffrey Mason, until Michael Aschbacher and Stephen Smith published a 1,221-page treatment in 2004. This is the "first-generation proof." A more systematic second-generation proof (Gorenstein, Lyons, Solomon, Capdeboscq) is incomplete, so Axiom formalized the first generation.

What was published

According to the project page, the proof follows the first-generation argument, with every logical step checked by the Lean kernel. The numbers: 43.1 million lines of Lean, 2.05 million declarations, and 715 papers and books in the corpus. The proof map also drew on the second-generation volumes. About 1.2 million lines come from the earlier Qiuzhen-CFSG project. The work also builds on Mathlib, the mathematics library for Lean. Key contributors are Dean Cureton, Vasily Ilin, Bhavik Mehta and Niels Voss. The principal investigator is Letong Hong.

The public GitHub repository describes the result as a "sorry-free" Lean 4 proof (no placeholders for unchecked parts), pinned to version 4.35.0-rc3 and based on Mathlib and the TauCeti project. It uses only the standard axioms Classical.choice, propext and Quot.sound, and no native_decide. The formal statement, translated, reads:

Every finite simple group is isomorphic to one of the explicitly constructed groups on the classification list.

lake build checks the entire development. Thanks to changes to the Lake build tool and planned optimizations, the build is meant to take under 24 hours. License: Apache-2.0.

How the 24 days unfolded

On October 1, 2026, Axiom set up a Slack channel. Existing Lean work and an internal proof map drawn from the literature split the project into 108 milestones and about 380 smaller tasks. The first swarm started on October 2. Agents claimed milestones via GitHub issues and reported progress in Slack. Lead agents broke down difficult arguments and checked statements. Others searched for existing results or wrote Lean proofs. Missing prerequisites could be delegated to further agents, whose results flowed into a shared repository.

Weak spots showed up early. Some seemingly feasible milestones hid huge prerequisites that the agents had merely assumed rather than proved. The team deleted tens of thousands of lines and restarted with a better plan. Build time also became a bottleneck, because agents delivered proofs faster than Lean could re-check them. Axiom distributed build caches across workers, ran checks in parallel and moved expensive finite computations into separately checkable certificates. The company says this sped up verification by orders of magnitude.

On October 10, a channel post reported that the agents had proved the Monster is simple. Its existence via the Griess algebra and an identification theorem were also formalized. On October 13, only one milestone closed. The team then broke open milestones into smaller, precise theorems, each with a short Lean proof showing how they combine into the milestone.

Gaps in the published proof

Translating the proof into Lean exposed problems in the original. Most were minor (typos, table errors, dropped hypotheses), but Axiom counts 34 notable deviations, the weightiest concerning the Unbalanced Group Theorem (UGT).

One example comes from the quasithin volumes by Aschbacher and Smith. A lemma claimed that two quantities were equal. The agents found a counterexample with the group SL₂(5), where one quantity was 1 where 2 would have been needed. An inequality fixed the lemma, but later arguments had used the equality to rule out cases. The team extended an earlier argument accordingly.

The UGT helps determine an entire group from information about its subgroups. According to the abstract of the companion paper, under the inductive assumptions of the classification, a nontrivial subgroup of odd order that is normal in the centralizer of an involution implies that the simple group is of Lie type in odd characteristic or alternating of certain degrees. Axiom went through John Walter's 1986 memoir and found explicit counterexamples to a closure claim used there. An operation that was supposed to keep simple groups within a certain family could produce an explicitly excluded group. Starting from PSL₂(49), whose field involution has centralizer PGL₂(7), you get the component PSL₂(7), which is excluded because 7 is a Mersenne prime. According to Axiom, these counterexamples refute neither the UGT nor Walter's Proposition II.5.9(ii).

The repair drew on Solomon's 1976 theory of maximal 2-components. From it, Axiom's AxiomProver system generated and formalized an alternative argument. The key step, Theorem 2.3 ("preservation of simple tops"), counts as a new result in group theory, according to Axiom. Together with reductions by Gilman and Solomon and recognition theorems by Foote and Harris, it yields the form of the UGT that the classification needs. After formalization, Axiom mathematicians found a shorter derivation (Remark 9.5) that doesn't need Theorem 2.3.

The paper "The Unbalanced Group Theorem" by Colin Defant and Ken Ono appeared on October 27, 2026 as version 1 on the Hexagon preprint server (CC BY 4.0, 35 pages). Axiom plans to collect errata with group theorists and publish them on an errata page. Lyons and Solomon were consulted on the UGT repair and sit on an advisory board together with Dan Nakano. Axiom stresses that the classification remains the achievement of the mathematicians who discovered the groups and developed the arguments.

Our take

The case shows that AI agents can produce formal mathematics at scale. It also makes a famous, hard-to-verify proof mechanically checkable. That errors surfaced in the published proof but could be repaired supports the value of formalization. Caveats remain: the claims come from the company itself, and independent verification of the statement and the errata is still pending. The Lean kernel's acceptance of the proof also depends on the formal statement capturing what was actually meant. It's also unclear how much of the achievement belongs to human planning and earlier projects such as Qiuzhen-CFSG and Mathlib. The second-generation proof remains incomplete.