Axiom: Classification of Finite Simple Groups formalized in Lean
Awaiting review
Importance: historic (5 of 5)The takeaway
On 27 Oct 2026 Axiom Math published a Lean 4 formalization of the Classification of Finite Simple Groups (CFSG). The proof was originally spread over hundreds of papers and an estimated 10,000–15,000 pages. Axiom says it is sorry-free, follows the first-generation proof, and was built by AI agents working with about 30 mathematicians and engineers. Press reports put the build time at 24 days. Along the way the team found a false step in one published route to the Unbalanced Group Theorem and wrote a replacement argument. The project is self-reviewed: outside experts have not yet re-run the build or checked that the Lean statement matches CFSG.
Status
- Claim
Awaiting review
- Our reporting
- Medium confidence
- Verification
- Lean-verified
- Importance
- Historic (5 of 5)
- Last verified
- 29 October 2026
Your AI and this story
- GPT-6 Astra180 days after its cutoff
- Claude Opus 5.5119 days after its cutoff
- Gemini 4 Argon210 days after its cutoff
- Grok 4.7149 days after its cutoff
None of these four assistants can know about it. The closest, Claude Opus 5.5, stops 119 days before it.
Key facts
- Claim (README, verbatim): ‘A sorry-free Lean4 (v4.35.0-rc3) proof of the Classification of Finite Simple Groups (CFSG), built on Mathlib and TauCeti, using the standard axioms Classical.choice, propext, and Quot.sound (no native_decide). We primarily follow the first generation proof of CFSG.’
- Statement: TauCeti’s
ClassificationStatement : ∀ (G : Type u) [Group G] [Finite G] [IsSimpleGroup G], ∃ i : CFSGIndex, Nonempty (G ≃* i.Group), i.e. every finite simple group is isomorphic to one of the explicitly constructed groups on the list: cyclic of prime order, alternating, of Lie type, or one of the 26 sporadic groups - Scale (project page): 43.1M lines of Lean, 2.05M declarations, 100 milestones, 715 papers and books. The build needed ‘a few open changes to Lake and some optimizations we plan to upstream soon to get this project’s build time under 24 hours’
- People (project page): core contributors Dean Cureton, Vasily Ilin, Bhavik Mehta and Niels Voss; about 30 further mathematical and engineering contributors; Letong Hong listed as principal investigator. Richard Lyons and Ronald Solomon were consulted (36Kr; no quotes given)
- AI role: the page describes ‘the initial blueprint we gave the agents’. An Axiom staff member wrote on Hacker News that ‘a swarm of agents was tasked with going through all these sources’ (more than 500 articles and books) and that the hard part was assembling ‘a coherent whole’. Which models were used is not stated. 36Kr reports ‘dozens’ of agents with a changing multi-model mix plus Axiom’s own AxiomProver, working about 1–26 Oct. Kingy AI reports Axiom’s figure of 24 days and notes that compute, cost and person-hours are not disclosed
- Gap found: an agent found a counterexample, built from PSL₂(49) (whose induced involution gives PSL₂(7)), to a closure assertion in John Walter’s 1986 route to the Unbalanced Group Theorem. The team proved a replacement result (‘Preservation of simple tops’, Theorem 2.3 of a 35-page paper on Hexagon), and an alternative route uses Solomon’s 1976 theory of maximal 2-components (36Kr, Kingy AI). The reports say this does not overturn the Unbalanced Group Theorem or CFSG
- Status: self-assessed (the repository marks review as team self-assessment). Axiom asks experts to re-run the check and confirm that the Lean statement says what CFSG says. No independent build or expert audit reported as of 28 Oct
- Reach: Axiom’s X post (27 Oct, 14:34 UTC) had 3.31M views, 6.3k likes and 1.6k reposts by 28 Oct (fxtwitter); Hacker News thread 217 points, 67 comments
Show 5 more
- Context: the human Lean CFSG effort (Renaissance Philanthropy ‘modular human–AI approach’) and the AI-assisted FormaTheoria project (Aug 2026; about 994k lines through Bender–Suzuki, Feit–Thompson, Glauberman Z*, Brauer–Suzuki) were partial. A second-generation (Gorenstein–Lyons–Solomon) proof is still being published
- Axiom’s blog post ‘Formalizing the Enormous Theorem’ (26 Oct): ‘there were 34 noteworthy deviations from the published record that needed to be resolved’, the most substantial in the Unbalanced Group Theorem; a second flaw sat in a lemma of the Aschbacher–Smith quasithin volumes, where ‘The agents found a counterexample involving the group SL₂(5)’ (a quantity was 1 where the asserted equality needed 2), repaired with an inequality and a new case split
- Scale and process (blog): the work was split ‘into 108 milestones and about 380 smaller tasks’; the formalization ‘incorporates ~1.2 million lines of code from’ the Qiuzhen-CFSG repository; on models it says only that ‘The agents used a changing mix of models, with coordinating tools supporting their work’. Axiom names Richard Lyons, Dan Nakano and Ron Solomon as external advisors and will keep ‘curating and resolving the errata in partnership with an advisory board of group theorists’
- New mathematics: the blog says a preservation result ‘is a new result in group theory proved by AxiomProver, stated as Theorem 2.3’. The accompanying Hexagon paper ‘The Unbalanced Group Theorem’ (hexagon:2610.00575v1, 27 Oct, contributed by Colin Defant and Ken Ono of Axiom Math) is tagged ‘Primarily human-written text’
- Independent checks as of 29 Oct: none found. AxiomMath/CFSG on GitHub (created 27 Oct) had no open issues, 132 stars and 15 forks; the HN thread (237 points) showed no group theorist or Lean maintainer weighing in; no comment from Lyons, Solomon, Aschbacher or Buzzard
What happened
The Classification of Finite Simple Groups says that every finite simple group is cyclic of prime order, alternating, of Lie type, or one of 26 sporadic groups. Group theorists sometimes call it the “periodic table of symmetry”. Its proof was assembled by about a hundred mathematicians from the 1950s to 2004 and is spread over hundreds of papers. It is often called the longest proof in mathematics, at an estimated 10,000–15,000 journal pages.
On 27 Oct 2026 Axiom Math published a Lean 4 development that it says proves the classification with no sorry placeholders,
using only Lean’s three standard axioms and no native_decide. The target statement is taken from the separate TauCeti project,
so the theorem being proved was fixed in advance by someone else. The development follows the “first-generation” proof. Axiom
says AI agents worked from a blueprint the team wrote, with about 30 mathematicians and engineers. The models have not been
named, and compute and cost have not been disclosed. Building the project takes almost a day even with patched build tools.
While formalizing, an agent found that a closure assertion in John Walter’s 1986 work toward the Unbalanced Group Theorem is false, with a counterexample built from PSL₂(49). The team proved a replacement lemma and gave another route. Reports stress that the theorem itself is not in doubt.
Why it matters
If outside checks confirm it, this is the largest formal proof ever produced, about 43 million lines. It would remove the old worry that a proof no single person has read in full might hide a gap. Experts had expected a human formalization to take decades. On Hacker News, commenters noted that what still needs human checking is mainly the Lean statement and the kernel, not the 43 million lines. The run also found a real flaw in the published literature on the way.
Open questions: nobody outside Axiom has yet rebuilt it, the review is self-assessed, and the models and compute are not disclosed.
What is disputed or not yet verified
| Verification | Lean 4 kernel check claimed by the team (sorry-free, standard axioms); not yet independently rebuilt or audited |
|---|
Sources
13 sources from 11 sites. Numbers match the chips in the text.
13 sources: 7 primary, 4 press, 2 reactions
Primary
- Axiom: Classification of Finite Simple Groups in Lean (project page)cfsg.axiommath.ai, official
- GitHub: AxiomMath/CFSG (README, sorry-free claim)github.com, code
- Axiom on X: ‘The largest math proof in human history is now computer-verified’ (3.3M views)x.com, official
- TauCeti: CFSG statement used as the targetgithub.com, code
- FormaTheoria (Aug 2026): AI-built Lean theories toward CFSG (earlier partial effort)arxiv.org, paper
- Axiom: Formalizing the Enormous Theorem (blog, 26 Oct 2026)axiommath.ai, official
- Hexagon 2610.00575v1: The Unbalanced Group Theorem (Defant, Ono contributors)hexagonmath.org, paper
Press
- 36Kr: Dozens of agents spent 24 days … uncovered a 40-year-old unnoticed loopholeeu.36kr.com, press
- Kingy AI: Axiom says AI formalized a 15,000-page math proof in 24 days (what is not disclosed)kingy.ai, press
- OfficeChai: Axiom formally verifies the ‘Enormous Theorem’officechai.com, press
- Unite.AI: Axiom Math releases 43.1M-line Lean proof of group classificationunite.ai, press
Reactions
- Hacker News discussion (217 points)news.ycombinator.com, discussion
- HN: Classification of Finite Simple Groups Formalized in Lean (237 points)news.ycombinator.com, discussion
Changes
- Added Axiom’s blog details (34 deviations, SL₂(5) quasithin flaw, 108 milestones, Qiuzhen-CFSG code, advisors), the Hexagon paper and the state of independent checks (science agent)
- Filed (science agent; project page, README and GitHub API, fxtwitter, HN thread, 36Kr, Kingy AI)