Axiom's Lean Proof of the Finite Simple Groups Theorem

On October 26, 2026, Axiom Math released what it calls "the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG)." Axiom says engineers and mathematicians directed swarms of dozens of AI agents for 24 days, and that the project produced approximately 43.1 million lines of code in the Lean proof assistant. The code is public in the AxiomMath/CFSG repository on GitHub (checked October 29, 2026), and an interactive proof map is at cfsg.axiommath.ai.

This post explains what the theorem is, what "computer-checked" means, how Axiom says its agents did the work, and what people still need to check.

What the classification says

A group, in math, is a set of moves that describe symmetry. Axiom's post uses a cube: there are 24 ways to rotate it so it looks the same as before, any two rotations combine into another one, and every rotation can be undone.

Finite groups break down into smaller pieces that cannot be split further. These pieces are the finite simple groups. Axiom calls them the "atoms" of finite groups and calls the classification "a periodic table of finite symmetry."

The theorem says every finite simple group is on one list:

• cyclic groups of prime order
• alternating groups on at least five symbols
• sixteen infinite families of "groups of Lie type," built over finite fields
• exactly 26 sporadic groups that fit no family (Axiom notes that some authors count the Tits group as a 27th)

The largest sporadic group, the Monster, has about 8 x 10^53 elements, according to Axiom. The hard part of the theorem is not finding the groups. It is proving that nothing is missing from the list.

The original proof is very large. Axiom writes that it "extends across roughly 15,000 pages in more than 500 articles by about 100 mathematicians" and that the result is "widely considered to be the longest mathematical proof ever written by humans." Daniel Gorenstein announced the classification complete in 1983, but a gap on the "quasithin" case stayed open until Michael Aschbacher and Stephen Smith published a 1,221-page treatment in 2004. That completed what is now called the "first generation proof." A reorganized "second generation proof" is still in progress; Axiom says ten volumes had appeared by 2023 and at least twelve are expected.

What Lean and formal verification mean

Lean is, in Axiom's words, "a programming language in which mathematical definitions, statements, and proofs can be written precisely enough for a computer to check every step." Axiom's project site says every logical step is "checked by Lean's kernel," the part of Lean that accepts or rejects proofs. Axiom notes that a human reader can supply a missing justification from experience, while formalization requires those choices to be made explicit: "When a necessary argument is missing, formalization does not proceed until the gap is closed."

Formal checking has reached this area before. Axiom notes that in 2012 a team led by Georges Gonthier finished a formal proof of the Feit-Thompson theorem, whose original proof ran to 255 pages, in the Coq (now Rocq) proof assistant after a six-year effort.

What Axiom did

Axiom chose to formalize the first generation proof, because the second generation proof is incomplete. The repository README describes "a sorry-free Lean4 (v4.35.0-rc3) proof" built on the Mathlib library and the TauCeti project. The final theorem uses a CFSG statement written by TauCeti: every finite simple group is isomorphic to one of the explicitly constructed groups on the classification list.

Axiom's project site lists 43.1M lines of Lean and 2.05M declarations. Axiom also says the project was built on pre-existing Lean work and "incorporates ~1.2 million lines of code from Qiuzhen-CFSG."

How the AI agents helped, per Axiom

Axiom gives this timeline and division of labor:

• On October 1, 2026, the team opened a Slack channel. Existing Lean work plus an internal "proof map" built from the literature split the job into 108 milestones and about 380 smaller tasks.
• On October 2, the first swarm went live. Agents claimed milestones through GitHub issues and reported finished work in Slack.
• "Lead agents decomposed difficult arguments and reviewed the statements being formalized. Other agents searched for existing results or concentrated on writing Lean proofs." The agents used "a changing mix of models." Axiom does not name the models.
• "Human mathematicians investigated mathematical obstructions, while engineers kept the growing system productive."

Axiom also describes what went wrong. Some milestones hid large prerequisites that agents "had assumed rather than proved," and the team "deleted tens of thousands of lines built on those assumptions." On October 13 only one milestone closed, so engineers ran a replanning effort that split unfinished milestones into smaller theorems. Build time was another limit: agents wrote proofs faster than Lean could recheck them, so engineers built a shared cache and moved expensive finite calculations into certificates checked separately. On October 10, the channel got the message "WE PROVED MONSTER IS SIMPLE."

What the formalization found

Axiom says turning the proof into Lean exposed problems in the published work. Most were minor: typos, errors in tables, dropped hypotheses. But it reports "34 noteworthy deviations from the published record."

The largest involved the Unbalanced Group Theorem. Axiom says its agents found counterexamples to a step in John Walter's 1986 argument, and stresses that these "did not refute the desired goal" of the theorem. With advice from group theorists Richard Lyons and Ronald Solomon, AxiomProver produced and formalized another route, including a result Axiom calls new: Theorem 2.3, "Preservation of simple tops," written up in a 35-page paper. Axiom adds that its mathematicians later found a shorter route that does not need Theorem 2.3.

Axiom says it will publish the full errata list "in consultation with several expert group theorists." As of October 29, 2026, the errata page on the project site says the list will be published there.

What mathematicians still need to check

A computer check is strong on some questions and silent on others. These are the open points, each tied to a source.

• Does the formal statement say what CFSG says? Axiom is direct about this: "Humans inspect that statement and the definitions it uses to confirm that it expresses the intended classification; Lean checks the formal deductions establishing it." In Axiom's division of labor, that check falls to people, not to Lean.
• What does the proof trust? The README says the proof uses only the standard axioms Classical.choice, propext and Quot.sound, with no native_decide. The Lean reference describes these as the standard additions to Lean's logic. It also warns that native evaluation, which native_decide uses, makes a proof depend on the correctness of the Lean compiler, not only on the kernel. Axiom says it avoided that tool.
• Are there unfinished steps? In Lean, sorry marks a step left unproved. The README says the proof is "sorry-free." Axiom also writes that progress was "easy to overstate during formalization," because Lean will check a result proved under an extra assumption that was never established.
• Can others reproduce it? The README says lake build builds the whole project, and that Axiom used "a few open changes to Lake and some optimizations we plan to upstream soon to get this project's build time under 24 hours." Axiom's post does not report an outside rebuild.
• Does it follow the historical proof? Axiom calls this "a separate question." Its Unbalanced Group Theorem route differs from Walter's published argument.

Why it matters, per Axiom

Axiom says results throughout algebra, number theory, combinatorics and mathematical physics use the classification, and the formal version lets a reader trace which results support a step and use the formal parts in later work. It credits the theorem to "the mathematicians who discovered the groups and developed the arguments that identify them," and says it will keep resolving errata with an advisory board that includes Lyons and Solomon.

For other AI and Lean math work on llms.blog, see our posts on the 3D Ghys conjecture proof with Lean verification and on Terence Tao's warning about AI proof abundance.

Sources

• Axiom: Formalizing the Enormous Theorem (October 26, 2026)
• AxiomMath/CFSG repository and README
• CFSG in Lean project site and proof map
• The Unbalanced Group Theorem, the accompanying 35-page paper on Hexagon (October 27, 2026)
• Lean reference: Validating a Lean Proof
• Theorem Proving in Lean 4: Axioms and Computation