Axiom's AI Agents Formalize the Classification of Finite Simple Groups in 24 Days

TL;DR

Axiom says it has released the first complete computer-checked proof of the classification of finite simple groups: about 43.1 million lines of Lean, written by "directed swarms of dozens of AI agents" between October 2 and October 25, 2026, and published as a sorry-free, Apache-2.0 repo on October 27. Along the way the agents logged 34 "noteworthy deviations" from the published 15,000-page proof, the biggest a closure claim in John Walter's 1986 route to the Unbalanced Group Theorem that has explicit counterexamples, now patched with a new theorem. The models, compute and cost are undisclosed, the statement covers one direction of the classification, and the Lean community's standing warning applies: a 43 million line proof is a certificate, not a library.

What actually shipped

The artifact is the AxiomMath/CFSG repository, created October 27 under Apache-2.0. The README calls it a "sorry-free Lean4 (v4.35.0-rc3) proof" built on Mathlib and the Tau Ceti project, following the first-generation proof of the classification. It uses Lean's three standard axioms (Classical.choice, propext, Quot.sound) and no native_decide, so nothing gets smuggled past the kernel through compiled code.

In Lean, sorry is the placeholder that lets a file compile with a hole in the argument. "Sorry-free" is a technical claim, not an attitude: every step is checked by the kernel. A sorry is an IOU in a ledger. The books balance, but only because someone promised to pay later. This ledger has none.

The companion site at cfsg.axiommath.ai is an interactive proof map and reports 43.1 million lines, 2.05 million declarations, and 715 papers and books in the source corpus. The build uses a modified Lake, and the README says planned optimizations are aimed at a full build in under 24 hours. Roughly 1.2 million lines come from Qiuzhen-CFSG, the Tsinghua University effort whose August paper, FormaTheoria, reported more than 994,000 lines reaching the Bender-Suzuki theorem after about seven months.

For scale: Anthropic's Fermat's Last Theorem formalization, which we covered in September, was about 13 million lines in 11 days. Gonthier's 2012 Coq proof of the Feit-Thompson Odd Order Theorem, the previous landmark in formalized group theory, took a team six years and runs to roughly 150,000 lines with libraries (the Lean eval page puts it at about 170,000). Feit-Thompson is a 255-page paper. The classification is around 15,000 pages across more than 500 articles by about 100 mathematicians, and the agents' corpus covered 715 sources.

How the swarm ran

Axiom's write-up is unusually specific about process. A Slack channel opened on October 1. The first agent swarm went live on October 2, working from a proof map split into 108 milestones and about 380 smaller tasks. Lead agents decomposed arguments and reviewed the statements being formalized; other agents searched the literature for existing results or wrote Lean proofs. Agents claimed milestones through GitHub issues, reported progress in Slack, and could delegate prerequisites to other agents. Results went into a shared repository. Human mathematicians investigated obstructions and reviewed the most consequential errata, and engineers kept the system running.

On October 10 the agents posted "WE PROVED MONSTER IS SIMPLE" to Slack, which is the only Slack message of 2026 worth pinning. On October 13, with only one milestone closed, the engineers launched a replanning pass that split the unfinished milestones into smaller theorems. The progress chart runs from October 2 to October 25, and the release went out on October 26.

Two engineering details matter more than the headline numbers. First, a distributed build cache spread compiled results across workers and reused them when code and dependencies were unchanged, so parallel agents weren't rebuilding the same tens of millions of lines. Second, expensive finite computations were pulled out of the main proof into certificates that Lean checks separately, which the team says sped up verification by orders of magnitude. The certificate trick is a restaurant inspection that checks the receipt and the thermometer log rather than recooking every dish: the kernel checks the witness and skips the search.

Early milestones, including the signalizer functor theorem, produced conditional proofs resting on unproved assumptions. Lean will happily verify a result under an unproven hypothesis, so the team tracked those explicitly, refused to count them as complete, and eventually deleted "tens of thousands of lines" of early assumption-laden work. The post names no models ("a changing mix"), no agent count beyond "dozens," no GPU hours and no bill.

What the agents found wrong in the literature

Humans had already patched the published proof for decades, so the interesting part is what a kernel-checked pass still turned up: 34 noteworthy deviations, most of them typos, table errors and dropped hypotheses. Two are substantive.

The first is in the Unbalanced Group Theorem, a central result in the first-generation proof that Walter's 1986 memoir is credited with establishing. The agents found explicit counterexamples to a closure assertion in that route: an operation assumed to stay inside a family of groups can produce one the family excludes. Axiom's worked example is PSL2(49), whose field involution has centralizer PGL2(7) with simple component PSL2(7), excluded because 7 is a Mersenne prime. The counterexamples do not refute the theorem itself, but they leave the needed inference unjustified. Axiom's fix is a new preservation theorem (Theorem 2.3, "Preservation of simple tops") in a 35-page companion paper, The Unbalanced Group Theorem, posted October 27 with Colin Defant and Ken Ono listed on it; Ono is Axiom's founding mathematician. A shorter deduction in the paper reaches the same conclusion without the new theorem.

The second is in Aschbacher and Smith's 1,221-page treatment of the quasithin case, where a lemma asserted two quantities were equal. SL2(5) is a counterexample: one quantity is 1, not 2. The repair replaced the equality with an inequality and revised the case division. The site's errata page is still a placeholder ("We are working with group theorists to compile the errata we found in the literature"), so the full list of 34 is not yet public.

What this is and isn't

The theorem is the Tau Ceti statement: every finite simple group is isomorphic to a cyclic group of prime order, an alternating group on at least five points, a group of Lie type, or one of the 26 sporadic groups. Only that direction is proven. The statement does not require showing the listed groups are finite, simple or non-redundant, and the formalization inherits the correctness of Tau Ceti's definitions. Humans checked that the formal statement says what it should; Lean checked the deductions.

It also formalizes the first-generation proof, not the cleaner Gorenstein-Lyons-Solomon second-generation project, which stands at ten volumes with at least twelve expected. Axiom's own post says the classification remains the achievement of the mathematicians who discovered the groups, and Richard Lyons and Ron Solomon, the L and S of that second-generation effort, were external advisors.

Seven Lean and Mathlib contributors published their position on swarm formalization ten days before this release. In How to Formalize All of Mathematics, Jeremy Avigad, Kevin Buzzard, Johan Commelin and four co-authors wrote that Anthropic's FLT code, "although the accomplishment is impressive," probably "has little ongoing value," that "the value of a formalization comes from our ability to use and interact with the data," and that the first principle should be to "defer to human-curated libraries, particularly Mathlib." The Hacker News thread made the same point in fewer words: "nice to know that the Classification is correct." Axiom's Jonathan Laurent replied there that the hard part was assembling 500-plus sources into a coherent whole, because the same informal concept gets formalized in slightly different, incompatible ways.

Context for the timing: Axiom raised a $200 million Series A led by Menlo Ventures in March at a $1.6 billion valuation, selling verified code generation to enterprises. A 43 million line kernel-checked proof is a loud demo that its prover scales.

Why builders should care

Strip the group theory out and this is the most detailed public account so far of running an agent swarm against an oracle that cannot be bluffed. The pattern is portable: a proof map decomposed into claimable issues, lead agents that decompose and review while workers search and write, Slack as the reporting bus, a shared build cache so parallel workers stop recompiling each other's output, expensive computation externalized into separately checkable witnesses, and a human replan at day 11 when the milestone count stalled at one. Replace "Lean kernel" with "a test suite the agent cannot edit" and the architecture is one you can copy this week.

The missing numbers are the ones you'd need to copy it honestly. Axiom names no models, gives no agent count, and publishes no token spend, cost or time per milestone. The 24 days show what a well-funded lab can do with undisclosed compute; nobody can turn them into a budget.

Key Takeaways

• Axiom released a sorry-free, Apache-2.0 Lean proof of the classification of finite simple groups: 43.1M lines, 2.05M declarations, standard axioms only, no native_decide.
• Swarms of AI agents did the writing between October 2 and 25, 2026, organized as 108 milestones and about 380 tasks claimed through GitHub issues; models, compute and cost are undisclosed.
• The pass found 34 deviations from the published proof, including counterexamples to a closure claim in Walter's 1986 route to the Unbalanced Group Theorem and a false equality in Aschbacher-Smith, both repaired.
• Only the "every finite simple group is on the list" direction is proven, against Tau Ceti's statement, following the first-generation proof rather than the second-generation volumes.
• Kevin Buzzard and six co-authors argued ten days earlier that machine-generated proofs at this scale have "little ongoing value" unless they become usable libraries; this one is a certificate first.
• The orchestration playbook (claimable issues, build cache, externalized certificates, a day-11 replan) is the reusable part for anyone running agent swarms against a hard verifier.

Sources: Axiom, Formalizing the Enormous Theorem, CFSG proof map and project site, AxiomMath/CFSG on GitHub, The Unbalanced Group Theorem (Hexagon 2610.00575), Lean eval: the classification of finite simple groups (Tau Ceti statement), Lean eval: Feit-Thompson odd-order theorem, FormaTheoria (arXiv 2608.10894), Qiuzhen-CFSG on GitHub, Xena Project, How to Formalize All of Mathematics, Hacker News discussion, Unite.ai, SiliconANGLE on Axiom's Series A