On October 26, 2026, Axiom Math released what it calls the first complete computer-checked proof of the classification of finite simple groups (CFSG), the theorem that lists every basic building block of finite symmetry. The original proof, Axiom notes, is widely considered the longest ever written by humans: roughly 15,000 pages in more than 500 articles by about 100 mathematicians. The company says its engineers and mathematicians directed swarms of dozens of AI agents for 24 days and ended with about 43.1 million lines of code in Lean, a proof assistant whose kernel checks every logical step.
The first major step of that proof, the 255-page Feit-Thompson theorem, took a team led by Georges Gonthier at the Microsoft Research-Inria Joint Centre more than six years to formalize, a project it finished in September 2012. Axiom’s code, posted on GitHub on October 27, builds on Lean’s Mathlib library and reuses about 1.2 million lines from Qiuzhen-CFSG, a project that had already formalized Feit-Thompson with AI assistance. No group outside Axiom has rebuilt the proof yet, its chief executive said the same day.
A periodic table of symmetry
A group, in the mathematical sense, collects the ways to transform an object without changing how it looks. Axiom’s example is a cube, which has 24 rotations that leave it looking exactly as before. Every finite group breaks down into pieces that cannot be split further: the finite simple groups, which Axiom calls the atoms of finite groups.
The classification lists those atoms: cyclic groups of prime order, alternating groups on at least five symbols, 16 infinite families known as groups of Lie type, and 26 one-off “sporadic” groups. The largest sporadic group, the Monster, has about 8 × 10⁵³ elements.
Daniel Gorenstein announced the classification complete in 1983 and later called it “the enormous theorem.” The announcement was premature. A gap in the so-called quasithin case stayed open until Michael Aschbacher and Stephen Smith published a 1,221-page treatment in 2004. “Most of the people who truly understood the proof are retired or no longer with us,” Axiom’s Vasily Ilin wrote on X on October 27.
Twenty-four days, 108 milestones
Axiom opened a Slack channel for the project on October 1. A proof map built from the published literature split the work into 108 milestones and about 380 smaller tasks. On October 2 the first swarm went live.
Agents claimed milestones through GitHub issues, lead agents broke hard arguments into parts and reviewed the statements, and others wrote the Lean proofs. Human mathematicians worked on the mathematical obstructions while engineers kept the system running.
The first plan showed its weaknesses early. Some milestones hid large prerequisites that the agents “had assumed rather than proved,” and the team deleted tens of thousands of lines built on those assumptions. On October 10 a message in the channel read “WE PROVED MONSTER IS SIMPLE.” On October 13 only one milestone closed, and the engineers had agents split the unfinished ones into smaller, precisely stated theorems.
Checking became the bottleneck. “Agents produced proofs faster than Lean could recheck them,” Axiom writes. Its engineers shared cached build results across machines and moved expensive finite calculations into certificates checked separately, which sped up verification “by orders of magnitude.”
34 noteworthy deviations
Most of what the agents flagged was minor: typos, errors in tables, dropped hypotheses. Axiom counts “34 noteworthy deviations from the published record” and plans to publish an errata list with group theorists. Ilin’s own count on X was broader: “We found hundreds of errors in the existing literature, and wrote a paper about the largest one, but overall the proof was correct.”
One case sits in Aschbacher and Smith’s quasithin volumes. A lemma claimed that two quantities were equal, and the agents found a counterexample in the group SL₂(5), where one quantity is 1 and the equality needed 2. The team swapped the equality for an inequality and reworked the cases that had relied on it.
The largest problem concerns the Unbalanced Group Theorem (UGT), which settles a substantial case of the classification. Working through John Walter’s 1986 memoir, the agents found explicit counterexamples to a “closure assertion” in his argument; one of them starts from the group PSL₂(49). That left “a key inference unjustified,” Axiom writes, without refuting the theorem.
The accompanying paper, posted October 27 under a CC BY 4.0 license, adds that “UGT also has other proofs.” John D. Cook summed it up on his blog on October 28: “The UGT, and the CFSG that depends on it, is correct, but the proof was flawed.”
The repair rests on Ronald Solomon’s 1976 theory of maximal 2-components, and Axiom consulted Solomon and Richard Lyons, two of the group theorists behind the original classification. Axiom says its prover produced and formalized the new argument, whose key step, Theorem 2.3 (“Preservation of simple tops”), it calls “a new result in group theory proved by AxiomProver.” The paper itself is labeled “primarily human-written.” After the formalization, Axiom’s mathematicians found a shorter route to UGT that does without Theorem 2.3.
Precedents
The Feit-Thompson formalization of 2012 ran to 170,000 lines, according to Microsoft Research. Thomas Hales, writing on Terence Tao’s blog on October 9, put the formal proof of the Kepler conjecture at about 20 human work-years and 500,000 lines. In the same post he noted that Anthropic’s autoformalization of Fermat’s Last Theorem, announced September 4, generated 13 million lines of Lean in 11 days.
Qiuzhen-CFSG, whose code Axiom reuses, described its method on August 11 in FormaTheoria, a preprint whose authors include Shing-Tung Yau: an AI-assisted workflow that built a machine-checked Lean development running through the Bender-Suzuki theorem and covering Feit-Thompson. In October, three teams posted AI-assisted proofs of a 31-year-old geometry conjecture, and Claude wrote machine-checked no-crash proofs across 123 open-source libraries in a few weeks. On October 26, the day of Axiom’s post, OpenAI published a claimed refutation of the Exponential Time Hypothesis with a Lean version that it says was ready one day after its model found the argument.
What has not been checked yet
The figures on the formalization itself, from the 24 days to the 34 deviations, come from Axiom. In a RuntimeWire article published October 27, chief executive Carina Hong answered the question of whether anyone outside the company had built and checked the proof: “Not yet. We are publishing the build artifacts to help and encourage external parties to independently reproduce it.” The repository says the build fits under 24 hours only with “a few open changes to Lake,” Lean’s build tool, which Axiom plans to upstream.
A kernel check confirms the deductions. Whether the formal statement says what mathematicians mean is a separate question. Hales wrote that Lean proofs “should never be believed until they have been checked by the kernel” and should not be accepted until “a human audit is performed to ensure statement fidelity,” a task he calls “generally massively easier than checking the proof itself.”
Axiom takes the statement of the classification from a separate project, TauCeti, and says humans inspect it. Its errata list is not online yet, and the UGT paper is a preprint.
What it means
Group theorists proved the classification decades ago, and Axiom’s Lean version reaches the same theorem. The speedup is in the checking. Trust in the theorem has rested on more than 500 articles and on a shrinking number of experts who knew how they fit together. Axiom has turned those articles into one Lean project that others can rebuild, plus a replacement for the published UGT argument and a promised errata list.
The main open items on the whole classification are now a rebuild by outsiders and a careful reading of one formal statement and the definitions behind it. Hales calls that kind of statement audit “massively easier” than checking a proof. Axiom says its build takes under a day, on its own tooling.
Hales also notes that the Navier-Stokes formalization announced in September has already been confirmed by more than a dozen proof-checkers. The next markers for the classification are of that kind: a rebuild outside Axiom, the published errata list, and what group theorists make of Theorem 2.3 once they have read the paper.
Sources
- Formalizing the Enormous Theorem, Axiom Math, October 26, 2026
- AxiomMath/CFSG: A Lean formalization of the Classification of Finite Simple Groups, Axiom Math, GitHub, October 27, 2026
- The Unbalanced Group Theorem, Axiom Math, contributed by Colin Defant and Ken Ono, Hexagon 2610.00575, October 27, 2026
- Post on X, Vasily Ilin (Axiom Math), October 27, 2026
- Theorem Proof Gains Acclaim, Rob Knies, Microsoft Research, October 11, 2012
- FormaTheoria: Constructing Large-Scale Lean Theories from Mathematical Literature, Tianjiao Nie et al., arXiv, August 11, 2026
- Axiom publishes Lean proof artifacts to support independent reproduction, Emerson Redding, RuntimeWire, October 27, 2026
- What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI, Thomas Hales, guest post on Terence Tao’s blog, October 9, 2026
Header image: chart by MACCUS, data from Axiom Math (October 26, 2026) and Microsoft Research (October 11, 2012)
