What Axiom Math claimed in October 2026, what a Lean proof can and cannot certify, and what is still unchecked.
In October 2026 Axiom Math announced a Lean proof of the Classification of Finite Simple Groups (CFSG), and said the Monster group was proved simple along the way. This chapter records what was announced, what a Lean proof does and does not certify, and what this book has and has not checked. Every statement about Axiom's work below is their claim, attributed to their post, and nothing here confirms it.
Claimed: yes, by Axiom Math, in a post dated 26 October 2026.
Lean-checked: asserted by Axiom. This book did not build the repository.
Independently verified: the post describes no independent verification. Three external advisors are thanked; the post does not say they verified the formalization.
Absorbed by the mathematical community: not yet, and not the kind of thing that happens in a week.
The post, "The Enormous Theorem, Formalized", says AI agents, directed by Axiom's AxiomProver system with human mathematicians and engineers overseeing, produced a complete computer-checked proof of CFSG in Lean using the Mathlib library. It gives these figures: about 43.1 million lines of Lean; 108 milestones and about 380 tasks; work began on 1 October and the first agent run on 2 October; the Monster group was proved simple on 10 October; one milestone closed on 13 October, followed by a replanning; the post is dated 26 October. About 1.2 million of the lines are reported to come from an earlier project, Qiuzhen-CFSG.
The theorem being formalized lists the finite simple groups: cyclic groups of prime order, alternating groups on five or more symbols, sixteen infinite families of Lie type, and the 26 sporadic groups (some authors count 27 by including the Tits group). The formalization follows the first-generation proof, because the second-generation proof is not finished.
The Monster $\mathbb{M}$ is the largest sporadic group, of order $2^{46}\cdot3^{20}\cdot5^{9}\cdot7^{6}\cdot11^{2}\cdot13^{3}\cdot17\cdot19\cdot23\cdot29\cdot31\cdot41\cdot47\cdot59\cdot71 \approx 8.08\times10^{53}$ (Chapter 8.0). Its smallest nontrivial irreducible representation has degree $196883 = 47\cdot59\cdot71$, which are the three largest primes dividing the order, and $196884 = 196883+1$ is the coefficient of $q$ in the $j$-function. The verifier script for this chapter checks that arithmetic, with controls that fail when the numbers are perturbed.
Axiom's post says the Monster's simplicity was proved on 10 October. This chapter cannot tell you how: the post, as retrieved, gave the date and not the argument, and the proof-map page I read never mentions the Monster. Simplicity of the Monster is a milestone in a 108-milestone plan, not the headline result.
A Lean proof is a program the kernel checks. If it compiles with no unproved placeholders and no extra axioms, the kernel certifies that the statement as written in Lean follows from Lean's foundations and the imported libraries. It does not certify that the Lean statement means what the English theorem means. Axiom's post says as much: human reviewers must check that the formal statement and definitions express the intended classification. And a result proved under an unstated extra assumption would also compile, which is why "no unjustified assumptions remain" is a separate claim from "it compiles".
This is not a hypothetical worry. Science's report of 13 October 2026 on OpenAI's release of 722 preprints says that, according to a mathematician quoted there, some of the Lean formalizations state something weaker than the main theorem, and that a preprint posted shortly before reported that the Lean file for OpenAI's Navier-Stokes result does not match the proof in its accompanying paper. Researchers quoted in the article say this does not mean the result is wrong. It does mean that "formalized" and "faithfully formalized" are different claims, and Olga Holtz is quoted there separating three states: claimed, independently verified, and understood and absorbed into mathematical culture. The table at the top of this chapter uses her distinction.
This project has caught the same failure in its own Lean files: theorems that compiled while proving something true but unrelated to their names (see “Do Not Trust, Verify”). The kernel was not wrong. The statement was.
The most mathematically interesting item in the post is not the speed. Axiom reports that while formalizing, its team found 34 noteworthy deviations from the published record, mostly small: typos, table errors, dropped hypotheses. The substantial one concerns the Unbalanced Group Theorem (UGT). The post says explicit counterexamples show a closure assertion in Walter's proof of the UGT fails, and that the team rerouted the argument rather than repairing that step. The rerouting rests on a new group-theory result in an accompanying paper (called "Preservation of simple tops", Theorem 2.3 there), and the paper also mentions a shorter deduction that avoids it.
If true, that is what formalization is for: a published proof of a deep theorem had a step that does not hold as stated, and the theorem survived by another route. I have not read the accompanying paper, I could not retrieve the errata page's list, and I have not checked the counterexamples. Treat the whole paragraph as a pointer to what to read, not as a finding.
| Source | Status |
|---|---|
| Axiom post | Read (via page-to-text summary, not the raw page). |
| Proof-map page | Read. It states 100 milestones in its summary and 108 in the Milestones header, without explaining the difference. It reports about 2.05 million declarations and 139 source works, and separately 715 papers and books, without reconciling those counts. |
| Errata page | Fetched; the list itself did not come back. The page only repeats the UGT story and says every step is checked by the Lean kernel, without saying whether any sorry or added axioms remain. |
| GitHub repository | Not opened. Building it and auditing axioms (#print axioms on the main theorem) is the check that matters most and has not been done here. |
| UGT paper (hexagonmath.org) | Not read. |
| Independent review | None found in the sources above. |
Four things, in order of cost. First, build the repository and run #print axioms on the main theorem; a clean result there is a statement about the kernel, and cheap to confirm. Second, have group theorists read the formal statement of CFSG and the definitions it depends on, the part Lean cannot check. Third, read the UGT paper and the counterexamples. Fourth, wait: Holtz's third state, absorption, takes years. Until the first two are done by someone other than the authors, "complete computer-checked proof" is a claim with a repository attached.
ch-monster-machine-checked-verify.py checks Monster arithmetic and the internal consistency of the figures reported by Axiom and by Science: that 2 to 25 October inclusive is 24 days, that 722 minus 3 withdrawn is 719, that 300 of 719 is 41.7 percent, and so on. Each has a control that fails if the number is perturbed. It never touches Lean. A figure that passes is self-consistent, not true.
Axiom Math, "The Enormous Theorem, Formalized", 26 Oct 2026
Axiom CFSG proof map and errata page
Tom Howarth, "OpenAI just changed math forever. Exactly how, no one yet knows", Science, 13 Oct 2026