Axiom's Lean formalization of the classification of finite simple groups: what it checks

Axiom Math says it has produced "the first complete computer-checked proof" of the classification of finite simple groups (CFSG), a theorem whose proof is often described as the longest in mathematics. According to its research post, over 24 days its engineers and mathematicians "directed swarms of dozens of AI agents" that wrote about 43.1 million lines of Lean, a language in which a computer checks every step of a proof. Along the way, the agents found counterexamples to a step in a 1986 route to one of the classification's key results, and Axiom published a new argument for that step. The post is dated 26 October 2026. The code, a paper and the announcement on X followed on 27 October, and a 57-page errata document on 28 October.

The announcement on X opens with "The largest math proof in human history is now computer-verified." That is a precise claim, and a narrower one than it may sound. Lean checks that a proof follows, step by step, from a formal statement and a short list of axioms. It does not check that the formal statement says what group theorists mean by CFSG, or that the 96 entries in the errata Axiom has published are right. And as of 30 October, we found no report that anyone outside Axiom has re-run the check. Axiom itself invites outside checks of the statement and of the build, and asks for corrections to the errata.

Below: what the theorem says, what Axiom released, what the Lean files establish, what Axiom found in the literature, how its counts differ between documents, and what is left for people. Every source was checked on 30 October 2026.

What is the classification of finite simple groups?#

A group is a collection of symmetries that can be combined and undone. Axiom's post uses a cube: 24 rotations leave it looking the same, doing two of them in a row gives another of the 24, and each can be reversed. Finite groups break down into pieces that cannot be broken down further, much as whole numbers break down into primes. Those pieces are the finite simple groups.

CFSG lists all of them. In the wording of Axiom's own paper: "Every finite simple group is either cyclic of prime order, an alternating group A_n for n ≥ 5, a simple group of Lie type, or one of the twenty-six sporadic groups". The largest sporadic group, the Monster, has about 8 × 10^53 elements.

The difficulty is the proof. Axiom's post describes it as "roughly 15,000 pages in more than 500 articles by about 100 mathematicians." Daniel Gorenstein announced the classification complete in 1983, but one case, the quasithin groups, stayed open until Michael Aschbacher and Stephen Smith published a 1,221-page treatment in 2004. A second-generation proof by Gorenstein, Richard Lyons, Ronald Solomon and later Inna Capdeboscq is still appearing; the post counts ten volumes by 2023 and expects at least twelve. Axiom's announcement thread puts the problem this way: "no one person has read the whole - it's too big."

What did Axiom announce?#

On 1 October, Axiom opened a Slack channel to coordinate the project, and the first "swarm" of agents went live on 2 October. Existing Lean work and a proof map assembled from the literature split the project into 108 milestones and about 380 smaller tasks. "Lead agents decomposed difficult arguments and reviewed the statements being formalized," while other agents searched for existing results or wrote Lean proofs. On 10 October the channel read "WE PROVED MONSTER IS SIMPLE." Not everything went forward. Some milestones turned out to rest on prerequisites the agents had "assumed rather than proved", and "We deleted tens of thousands of lines built on those assumptions."

On the AI side, the post says only that "The agents used a changing mix of models, with coordinating tools supporting their work." It names no model. On the human side: "Human mathematicians investigated mathematical obstructions, while engineers kept the growing system productive." The project site lists 31 contributors, four of them as core contributors.

The formalization builds on Mathlib, Lean's main mathematics library, and on Tau Ceti, a second library described below. The post says it also incorporates about 1.2 million lines from Qiuzhen-CFSG, an earlier open project whose README lists the Feit–Thompson, Bender–Suzuki and Gorenstein–Walter theorems as finished.

The release came in pieces:

What do the Lean files actually establish?#

The statement, and where it came from

The repository's headline theorem, CFSGComparator.classification in Comparator/Solution.lean, proves TauCeti.ClassificationStatement, which the README quotes:

def ClassificationStatement : Prop :=
  ∀ (G : Type u) [Group G] [Finite G] [IsSimpleGroup G],
    ∃ i : CFSGIndex, Nonempty (G ≃* i.Group)

In words: for every finite simple group G, there is an entry i on a list such that G is isomorphic to the group that entry defines. The list, CFSGIndex, has four kinds of entry: cyclic groups of prime order, alternating groups on at least five letters, groups of Lie type built from explicit algebraic data, and the 26 sporadic groups, each given by a finite presentation (generators and the relations between them).

Axiom did not write this statement. It comes from Tau Ceti, a Lean library "incubated by the Lean FRO and the Mathlib Initiative", where "Humans own the roadmap" and "AIs own the code". Tau Ceti's roadmap for the statement was added on 8 August 2026, and the statement itself was merged on 25 September. Axiom's repository pins Tau Ceti at a commit from 2 October. So the statement was written for another project, and was public before Axiom's project began on 1 October.

The statement goes in one direction. It says every finite simple group is on the list. The Tau Ceti file is explicit about what it leaves out: "No finiteness or simplicity property of a listed carrier is asserted here". Tau Ceti's roadmap leaves "Finiteness, simplicity, orders" of the listed groups to "downstream work". Axiom's repository also proves a second, broader theorem, in Axiom's own definitions, that adds that the groups on its list are finite and simple. Reading that one means reading Axiom's definitions as well.

Axioms, and no native_decide

The README says the proof uses "the standard axioms Classical.choice, propext, and Quot.sound (no native_decide)." These are the axiom of choice, propositional extensionality and the soundness of quotients. Lean can list the axioms any theorem depends on, so an extra, hidden assumption would show up.

native_decide is a shortcut for large computations. The Lean reference warns that it "adds the entire lean compiler to the trusted part, and a new axiom will show up in #print axioms". Avoiding it keeps the trusted part to Lean's kernel, which checks every proof, and the three axioms. Axiom says it moved expensive finite calculations into "certificates that could be checked separately". The certificate file we opened uses decide +kernel, which has the kernel do the computation itself.

Sorry-free, and the Lean version

In Lean, sorry is "a temporary placeholder for an incomplete tactic proof". A file with a sorry still compiles, with a warning, and every theorem that depends on it picks up the axiom sorryAx. "Sorry-free" means no step was left as a placeholder, and the axiom list above is the check: sorryAx is not on it. The repository's metadata file records sorry_count: 0.

The one deliberate sorry is in Comparator/Challenge.lean, which states the target with no proof. A configuration file tells Lean's comparator tool to check that the solution proves exactly that statement, with only the three permitted axioms, and that the kernel accepts it. Since Lean 4.35.0 this check ships with Lean, as lake comparator, according to the tool's README.

The project builds with Lean v4.35.0-rc3, a release candidate, and pins Mathlib and Tau Ceti to exact commits, so a rebuild can use the same toolchain, libraries and statement.

The same metadata file also says how the work was reviewed: status: self-assessed, with reviewers: ["Axiom Math"], and automation method: autonomous, framework: "AxiomProver".

On the last row, the post itself says: "Whether a formal development reproduces each step of a particular historical argument is a separate question".

What did Axiom find in the literature?#

The agents logged suspected problems as they went. Most, the post says, "turned out to be innocuous: typos, errors in tables, dropped hypotheses, or steps that are clear from context. A few required real mathematics." In one lemma from Aschbacher and Smith's quasithin volumes, for the group SL₂(5), "one quantity was 1 where the asserted equality required 2."

The Unbalanced Group Theorem

The largest case concerns the Unbalanced Group Theorem (UGT). Axiom's paper summarizes it: under the inductive hypotheses of the classification, "a nontrivial subgroup of odd order normal in the centralizer of an involution forces the ambient simple group to be a group of Lie type in odd characteristic or one of the alternating groups of certain degrees." An involution is an element of order two. In the paper's words, "UGT therefore removes all unbalanced groups from the remaining classification problem."

Because Axiom chose to follow the first-generation proof, it worked through John Walter's 1986 memoir, one of the published routes to UGT. Walter defines a family of groups PSL₂(q), with q odd and excluding 9, Fermat primes and Mersenne primes. His argument asserts that a certain operation, taking the component of an involution's centralizer, keeps you inside that family. The agents found that it does not when the involution is a field automorphism:

The paper is careful about scope: "Namely, we have identified a gap in this inference, not a counterexample to the proposition itself or to UGT." It also says "This difficulty does not obstruct CFSG", and names other routes to UGT: Gorenstein's account in his 1983 volume, following an argument of Morton Harris, and a deduction from the second-generation work of Gorenstein, Lyons and Solomon.

The new argument on Hexagon

Axiom needed a replacement that fit the first-generation proof it was building. The result is The Unbalanced Group Theorem, a 35-page paper whose title page reads "Axiom Math". It was deposited on Hexagon, a repository for mathematics research, on 27 October. Hexagon names Colin Defant and Ken Ono as contributors, both of whom appear among Axiom's mathematical contributors, and shows two declarations: "Primarily human-written text" and "Human understanding: all parts".

Its main result is Theorem 2.3, "Preservation of simple tops". Axiom's post calls it "a new result in group theory proved by AxiomProver". The paper also records, in Remark 9.5, that the same reductions allow a shorter deduction of UGT that does not need Theorem 2.3. The post says Axiom's mathematicians found that shortcut after the formalization. The paper keeps the longer argument "because AxiomProver formalized this route".

The role of Lyons and Solomon

Lyons and Solomon both worked on the original classification. According to Axiom's post, they were consulted on the arguments, and the UGT repair "benefited from correspondence with Lyons and Solomon." The post also says "Lyons helped clarify the available proof routes and place the obstruction in its historical context. Solomon's 1976 theory of maximal 2-components supplied the central ideas for the alternative argument that AxiomProver produced and formalized." The paper thanks Lyons, Dan Nakano and Solomon in its acknowledgments, and Axiom says it will keep curating the errata with "an advisory board of group theorists, including Richard Lyons and Ronald Solomon."

These descriptions are Axiom's. We found no public statement by Lyons or Solomon about the formalization.

How many corrections did Axiom report?#

Different documents give different figures:

The size of the code also varies. The post and the project site give 43.1 million lines of Lean; the X thread says "50 million lines of Lean".

Only the errata document says what it counts. Its first page reads: "The 96 entries record selected mathematical departures and elaborations. They are not a tally of 96 errors or new discoveries. This is not a comprehensive errata list." Routine typographical corrections, notational changes and "readily repaired slips are omitted." Part A holds 34 entries on "structural changes and alternative proofs", the same number as the research post's count. Part B holds 62 on "additional arguments and local corrections". The document says these categories "describe the extent of the change to the argument, rather than a measure of error or mathematical importance."

The errata also states how it was made: "This document was generated by the AI system AxiomProver." It adds that "AxiomProver autonomously produced all the corrections, supplementary arguments, and alternative proofs described here," and that "Some corrections were already known, and their inclusion makes no claim of priority."

What is still a human job?#

Reading the statement

Axiom's post divides the work this way: "Humans inspect that statement and the definitions it uses to confirm that it expresses the intended classification; Lean checks the formal deductions establishing it." On X, Axiom asked for exactly that: "We invite group theorists and the Lean community to validate it: rerun the proof check, and confirm that the Lean statement says what CFSG says."

Why it matters: a statement of this shape is only as good as its list. If one of the list's definitions described a different group from the one intended, the theorem would say something other than CFSG, and Lean would accept the proof all the same. Tau Ceti's roadmap says the same about its own definitions: "These requirements are enforced by review, not mechanically". It explains that Lean's axiom check "cannot distinguish an honest construction from one that selects a carrier from the target existence theorem," so "Reviewers of each work item must read the definitions and trace the carrier back to the explicit data". Tau Ceti's own status page, generated on 25 October, lists one part of that work as partial: matching the Lie-type constructions to the standard group schemes is done for some families and not yet for others.

Rebuilding it

The README gives one command, lake build, and a note: "We 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." Asked by the news site RuntimeWire on 27 October whether anyone outside Axiom had built and checked the proof, Axiom's CEO, Carina Hong, answered by email through a spokesperson: "Not yet. We are publishing the build artifacts to help and encourage external parties to independently reproduce it." By 30 October we found no public report of a complete outside rebuild. We checked the repository's issues and pull requests and searched the web.

Reviewing the errata and the new theorem

The 96 errata entries were generated by an AI system and cover decades of literature. Whether each entry is right, whether a simpler fix exists, and whether it was already known are questions for group theorists. The errata asks for that help: "We welcome corrections, references to earlier treatments, and suggestions for simpler arguments or further mathematical study." The UGT paper is a preprint; reading its new theorem as mathematics is separate from Lean accepting it.

What have mathematicians said so far?#

Timothy Gowers wrote on X on 27 October: "Given the history of uncertainty about whether the proof of CFSG was 100% correct, this seems like great news, even if the formalization itself is horrible. (I don't know whether it actually is horrible, but that would be my guess.)"

John D. Cook, who writes about mathematics on his blog, wrote on 28 October: "The UGT, and the CFSG that depends on it, is correct, but the proof was flawed." That is commentary on Axiom's materials, not a check, and Axiom's paper words the finding more narrowly: a gap in one published route, with the conclusion of Walter's proposition and UGT itself not refuted.

How can a result like this be recorded so others can check it?#

Much of what a checker needs is already public: the exact toolchain, library commits pinned in the build files, a statement taken from outside the project, a comparator configuration and a dated errata document. The history is harder to see. The public repository has a single commit, "Initial commit," made on 27 October. The 24 days of work the post describes, coordinated in Slack and in GitHub issues, are told in the post rather than published with the code, and the models are not named.

A record that others can check would tie together the exact commit and toolchain, the statement and the commit it came from, the axioms used, the date each piece became public, who did what (people and AI, with the models named), and who has checked what, with the outcome of each check. For CFSG, such checks may come over months, from different people, in different places.

Papex is built for part of this: hypotheses, findings and publications linked to the people, tools and versions behind them, signed by the person accountable and dated. Papex does not check proofs; Lean does that, and people check the statement. CFSG is a theorem, not an open problem, so it is not on our problem list or on the page where we list AI-assisted claims on open problems.

Sources#

• Formalizing the Enormous Theorem (Axiom Math, research post dated 26 October 2026), checked 30 October 2026
• AxiomMath/CFSG: README, lean-toolchain, lake-manifest.json, comparator.json, formalization.yaml, Comparator/Challenge.lean, Comparator/Solution.lean, Certificates/Certificate1.lean, CFSG/Milestones/CFSG_classification.lean (GitHub, commit 69cb972f, 27 October 2026), checked 30 October 2026
• CFSG in Lean, project site (Axiom Math), checked 30 October 2026
• Selected Departures from Published Arguments: Notes on the formalization of the classification of finite simple groups (Axiom Math, 28 October 2026), errata page and PDF, checked 30 October 2026
• The Unbalanced Group Theorem, hexagon:2610.00575v1 (Axiom Math; contributed by Colin Defant and Ken Ono; 27 October 2026), checked 30 October 2026
• Axiom (@axiommathai), announcement thread on X, 27 October 2026, including the posts on lines of Lean, the proof's size, UGT and errata and the invitation to check, checked 30 October 2026
• @andrew_v10209 on X, 27 October 2026, checked 30 October 2026
• Timothy Gowers (@wtgowers) on X, 27 October 2026, checked 30 October 2026
• John D. Cook, The Unbalanced Group Theorem (28 October 2026), checked 30 October 2026
• Emerson Redding, Axiom publishes Lean proof artifacts to support independent reproduction (RuntimeWire, 27 October 2026), a news report, used for Carina Hong's emailed reply; checked 30 October 2026
• Tau Ceti README (GitHub), checked 30 October 2026
• Tau Ceti, CFSG/Classification.lean at commit 6e0c6ac (2 October 2026), with its history and pull request #8792 (merged 25 September 2026), checked 30 October 2026
• Tau Ceti roadmap, CFSGStatement README (added 8 August 2026) and STATUS (generated 25 October 2026), checked 30 October 2026
• Qiuzhen-CFSG README (GitHub), checked 30 October 2026
• leanprover/comparator README (GitHub), checked 30 October 2026
• Tactic Reference: decide, native_decide and sorry (Lean Language Reference), checked 30 October 2026