Axiom Math says a swarm of AI agents has delivered a full proof, verified by computer, that the catalogue of finite simple groups is complete, a result so long that mathematicians nicknamed it “the enormous theorem.” The company laid out the work in a research post dated 26 October 2026. Over 24 days, its engineers and mathematicians directed dozens of agents that wrote some 43.1 million lines in Lean, a language built so that software can verify each step of a proof.
The math is easier to picture than the name suggests. A cube can be turned 24 different ways and still look unchanged. Do two of those turns in a row and you end up at one more of those 24 positions, and any turn can be undone. A collection of moves with those two traits is a group, and mathematicians use groups to describe symmetry.
Some groups can be broken into smaller pieces, and the ones that cannot be broken down further are called simple groups: the atoms. The classification is the complete catalogue of those atoms, a periodic table of symmetry. It has the simplest circular groups, one for each prime number, the shuffling groups on five or more items, sixteen infinite families, and 26 one-off oddities called sporadic groups. The biggest oddity, the Monster, has roughly 8 x 10^53 elements.
Proving that the catalogue has no missing entries took decades and about 100 mathematicians. The original argument runs to roughly 15,000 pages across more than 500 articles. Axiom’s post notes that the 1983 announcement of completion turned out to be premature, and a gap stayed open until a 1,221-page treatment appeared in 2004. Nobody could easily confirm the whole thing fit together, because results sat in papers written across several decades in different notation.
Axiom started on 1 October 2026 with a map of the published proof, cut into 108 milestones and roughly 380 small tasks. Agents claimed tasks through GitHub issues and handed prerequisites to other agents. Early on, some milestones turned out to hide enormous assumptions, and the team threw away tens of thousands of finished lines that rested on them. On 13 October only one milestone closed. Build times became the next bottleneck, so engineers cached results across machines and moved heavy calculations into separately checked certificates.
The more interesting output is what the machines found wrong. Axiom says most issues were typos, table errors, or dropped hypotheses, but 34 departures from the published text were serious enough to need real resolution. The biggest involved the Unbalanced Group Theorem. Concrete counterexamples turned up in a step of John Walter’s 1986 proof, though the theorem itself was not refuted. With advice from group theorists Richard Lyons and Ronald Solomon, Axiom’s prover wrote a different argument built on Solomon’s 1976 work, which the company says adds a new theorem to group theory. Its own mathematicians later found a shorter route that skips it.
For scale, Georges Gonthier’s team needed six years to formalize the 255-page Feit-Thompson theorem in 2012, one early landmark on the road to the full classification. Axiom’s 24 days covers a far larger body of work, though the company credits earlier Lean libraries and about 1.2 million lines of existing code it built on.
Every figure here comes from Axiom’s own post, which mentions no outside audit yet. Lean also checks the deductions, not the question: Axiom says humans still have to read the formal statement to confirm it says what the classification actually says.
Once the errata list goes public, group theorists can test Axiom’s count of 34 for themselves, and the first outside verdict on this approach will come from them.
Reported by Axiom Math in a research post dated 26 October 2026.
