# Axiom Says It Formalized the Classification of Finite Simple Groups in Lean in 24 Days; No Outside Group Has Rebuilt the Proof Yet

Times of AI Desk · 2026-10-28 · Research

[https://timesof.ai/2026/10/axiom-lean-formalization-classification-finite-simple-groups](https://timesof.ai/2026/10/axiom-lean-formalization-classification-finite-simple-groups)

> Axiom Math said on October 26 that it has produced the first complete computer-checked proof of the classification of finite simple groups, about 43.1 million lines of Lean written over 24 days by people directing swarms of AI agents. Axiom says the work exposed 34 noteworthy deviations from the published proof and produced a new group-theory result. Axiom's chief executive told RuntimeWire that no outside party has yet independently rebuilt and checked the proof.

Axiom's claim is checkable in principle: the Lean code is public, and Lean's kernel either accepts the proof or it does not. The step that has not happened yet is the one that matters most. Axiom's chief executive says no one outside the company has rebuilt the proof and confirmed it.

## What Axiom says it did

Axiom Math said on October 26 that it has formalized the classification of finite simple groups in the Lean proof assistant, which it calls "the first complete computer-checked proof" of the theorem. The classification says every finite simple group is cyclic of prime order, alternating, one of 16 infinite families of Lie type, or one of 26 sporadic groups. Axiom says the original proof runs to about 15,000 pages in more than 500 articles by about 100 mathematicians, and that it is widely considered the longest proof ever written by humans.

Axiom says engineers and mathematicians directed swarms of dozens of AI agents over 24 days, producing about 43.1 million lines of Lean. The project site lists 2.05 million declarations. Axiom says the formalization follows the "first generation" proof, completed in 2004, and that the code incorporates about 1.2 million lines from an earlier project, Qiuzhen-CFSG, and builds on Mathlib, Lean's community math library.

## What the formalization turned up

Axiom says translating the proof exposed problems in the published arguments. Most were minor, such as typographical errors, errors in tables or dropped hypotheses, but Axiom counts 34 "noteworthy deviations from the published record." The most substantial involved the Unbalanced Group Theorem, where Axiom says its agents found counterexamples to a step in John Walter's 1986 argument, though not to the theorem itself.

Axiom says its AxiomProver system produced an alternative argument for that step, built on ideas from Ronald Solomon's 1976 work, and that it amounts to a new result in group theory. It says group theorists Richard Lyons and Ronald Solomon were consulted on the arguments, and that it will publish the errata list in consultation with them.

## What has been checked independently

The Lean code is public on GitHub under the Apache 2.0 license; the repository was created on October 27. Carina Hong, Axiom's founder and chief executive, told RuntimeWire that no outside party has yet independently built and checked the proof. "Not yet. We are publishing the build artifacts to help and encourage external parties to independently reproduce it," she said, in an email sent through a company spokesperson.

Axiom says humans inspect the formal statement of the theorem and the definitions it uses, while Lean checks the deductions. An outside check would need to confirm both that the 43.1 million lines compile and that the final statement says what the classification says.

Axiom's announcement came on the same day that [OpenAI said its models had refuted the Exponential Time Hypothesis, a claim it also backed with Lean proofs](https://timesof.ai/2026/10/openai-claims-eth-refuted-local-smoothing-qft-proofs) and for which we found no independent verification.

## Limits

- The completeness claim, the line and declaration counts, the 34 deviations and the new result are Axiom's. We found no independent rebuild or expert review of the full formalization.
- We did not compile the Lean repository ourselves.
- The errata list has not been published in full. Axiom says it is still working through it with an advisory board of group theorists.
- Axiom's research post is dated October 26, while its GitHub repository was created on October 27.

## Sources

- [Axiom: Formalizing the Enormous Theorem (October 26, 2026)](https://axiommath.ai/research/the-enormous-theorem-formalized/)
- [Axiom: CFSG in Lean project site (October 26, 2026)](https://cfsg.axiommath.ai/)
- [GitHub: AxiomMath/CFSG (October 27, 2026)](https://github.com/AxiomMath/CFSG)
- [RuntimeWire: Axiom publishes Lean proof artifacts to support independent reproduction (October 27, 2026)](https://runtimewire.com/article/axiom-s-ceo-says-no-one-outside-the-company-has-rebuilt-its-43-million-line-proo)
- [Times of AI: OpenAI Claims Its Models Refuted the Exponential Time Hypothesis (October 27, 2026)](https://timesof.ai/2026/10/openai-claims-eth-refuted-local-smoothing-qft-proofs)