Axiom Math, a San Francisco-based company building AI systems for mathematics, has released the first complete computer-checked proof of the Classification of Finite Simple Groups (CFSG), widely described as the longest proof in the history of mathematics. According to the company's announcement, engineers and mathematicians directed swarms of dozens of AI agents over just 24 days to produce approximately 43.1 million lines of code in the Lean proof assistant, verifying a result that previously spanned roughly 15,000 pages across more than 500 journal articles written by about 100 mathematicians over several decades.
The achievement lands at a moment when machine-assisted mathematics is accelerating rapidly, and outlets tracking AI research news have watched formal verification move from a niche practice to a frontier capability. What makes this release unusual is scale: the formalization contains roughly 2.05 million declarations organized into 100 milestones, every one of them checked by Lean's kernel, the small trusted core that verifies each logical step.
What the Classification Actually Says
Finite simple groups are the indivisible building blocks of finite symmetry, and the classification — nicknamed "the enormous theorem" — gives a complete list of them. According to the project's documentation, every finite simple group is one of four kinds: a cyclic group of prime order, an alternating group on at least five symbols, one of sixteen infinite families of groups of Lie type constructed over finite fields, or one of exactly 26 sporadic groups that fit into no family.
Proving that this list exhausts every possibility took the better part of a century of collective effort. John Thompson, whose work was central to the classification, received the Fields Medal in 1970 and the Abel Prize in 2008. The proof was so long and so distributed across papers and generations of mathematicians that lingering doubts about its completeness persisted for decades — doubts this formalization now formally dispels.
Swarms of Agents Across 500 Sources
The original proof is scattered across more than 500 articles and books, many written decades ago in incompatible notations. An Axiom engineer described the method in the Hacker News discussion of the release: a swarm of agents was tasked with going through all of these sources, with the hard part being assembling everything into a coherent whole, since the same informal concept can be formalized in slightly different but mathematically incompatible ways.
The company's blog post states that the effort took 24 days from start to release, with human engineers and mathematicians steering the agent swarms rather than working line by line. The result follows earlier high-profile auto-formalization milestones in 2026, including Lean proofs of major classical theorems produced with frontier models, but at a scale no previous project has approached.
34 Deviations From the Published Record
Translating the published proof into machine-checkable form exposed real problems in the mathematical literature. Axiom reports that most issues were minor — typographical errors, mistakes in tables, or dropped hypotheses. But there were 34 noteworthy deviations from the published record that needed to be resolved before the formalization would go through.
The most substantial concerned the Unbalanced Group Theorem. While formalizing a first-generation route to the result, the team found counterexamples to a closure assertion used in a published argument. In consultation with expert group theorists, they constructed an alternative route built on Daniel Gorenstein-era structural techniques — specifically theory of maximal 2-components from the 1970s — and published the fix as a new 35-page group theory paper, posted as preprint 2610.00575. The company says it will release a lengthy errata list for the benefit of the mathematical community, compiled in consultation with the group theorists on whose work the classification rests.
Why Machine-Checked Mathematics Matters
The value of a formalization is not just that a computer approved the proof. A Lean formalization reduces the trust base to the proof assistant's kernel — a small, heavily audited program — instead of the accumulated confidence of thousands of pages read by scattered specialists. Commenters on the Hacker News thread, where the story drew hundreds of upvotes, noted that empirical knowledge of why the classification holds was at risk of literally dying out as the original generation of mathematicians retired, because no single person could hold the whole argument in their head.
There are practical echoes elsewhere in physics as well. The largest of the 26 sporadic groups, the Monster group, appears in the "monstrous moonshine" program connecting finite symmetry to modular functions — work that earned Richard Borcherds a Fields Medal in 1998 — and in Edward Witten's 2007 proposal linking the Monster's symmetries to black-hole entropy in a simplified three-dimensional universe. A verified classification puts the underlying structural mathematics on firmer ground for exactly these kinds of cross-disciplinary applications.
What Comes Next
Axiom says more papers derived from the formalization are on the way, alongside the errata project. For the formal methods community, the release sets a new benchmark for what agent-directed verification projects can attempt; for mathematics, it converts a sprawling, half-century-long collaborative achievement into a single artifact that any computer can check. The classification is no longer merely believed. It is now, in the most literal sense, proven — and the proof is available for anyone to download and verify.
