AI-assisted math results continue to stream in thick and fast.
San Francisco-based AI startup Axiom says it has produced the first complete, computer-checked proof of the Classification of Finite Simple Groups (CFSG), a result so large it earned the nickname “the enormous theorem” decades before any AI was involved in math research. The original proof, built up by around 100 mathematicians, runs across roughly 15,000 pages spread over more than 500 papers. Axiom says it rewrote the entire argument in a language a computer can check line by line, using swarms of AI agents that worked for 24 days and wrote about 43.1 million lines of code in the process.
What the ‘Enormous Theorem’ actually says
Groups are one of the first big ideas students meet in abstract algebra, and they show up everywhere symmetry does. Take a cube: there are 24 different ways to rotate it so it looks exactly as it did before you touched it. Combine any two of those rotations and you get another one on the list; every rotation can also be undone. That closed, reversible structure is a group. A shuffled deck of cards gives a much bigger example of the same idea.
Just as whole numbers break down into prime factors, finite groups break down into smaller indecomposable pieces, and the “primes” of group theory are called finite simple groups. CFSG is the full list of every possible finite simple group there is — mathematicians sometimes describe it as a periodic table for symmetry. It says the list consists of a few well-understood infinite families (prime-order cyclic groups, a family called alternating groups, and sixteen families built from finite number systems), plus a set of 26 oddball exceptions called sporadic groups. The largest of these, the Monster group, has roughly 8 × 10^53 elements and turns up in surprising places, including a construction in mathematical physics that Edward Witten once proposed could describe gravity in a simplified toy universe.
Proving that this list is actually complete — that no finite simple group has been missed — took from the 1950s, when Richard Brauer laid out the core strategy, through Daniel Gorenstein’s 1972 roadmap, to a 1983 announcement that the job was done. That announcement turned out to be premature: a gap involving so-called quasithin groups wasn’t closed until 2004, and smaller fixes kept surfacing well after that.
What “formalizing” it means, and why it matters
A proof this long, written by this many people over this many decades, is almost impossible for any single mathematician to fully audit. Formalization is the fix: the entire argument is rewritten in a language called Lean, where every definition, every hypothesis and every logical step has to be spelled out precisely enough for software to verify it. Nothing can be waved through as “clearly true.”
That process is unforgiving in a useful way, and Axiom’s agents found it. Most problems were small — typos, mislabeled tables, a dropped assumption here or there — but 34 were serious enough to need real repair work, and one, tied to something called the Unbalanced Group Theorem, required an entirely new piece of mathematics to fix cleanly. Axiom says it brought in group theorists who worked on the original classification, including Richard Lyons and Ronald Solomon, to help route around the gap, and the resulting argument has been written up as a new, separately citable result in group theory. Axiom is also publishing the full error list it uncovered for the wider math community to use.
For a field that depends on trust built up over generations of peer review, that’s the real headline: a 40-year-old, widely cited theorem still had unresolved cracks in its published record, and it took an AI system methodically checking every line to surface and patch them. It’s part of a broader pattern this year of AI labs chasing marquee, formally verifiable results in math — OpenAI claims to have proven a version of the Yang-Mills existence problem, and OpenAI and Anthropic both separately reported disproving the Exponential Time Hypothesis within hours of each other. Whatever one makes of each individual claim, the underlying computer-science question Axiom is also circling is the same one: can AI systems move from merely generating plausible-sounding proofs to producing ones a machine can certify are actually correct, at a scale no human team could check by hand.