Axiom Math formalizes the "Enormous Theorem" in 43.1M lines of Lean in 24 days

Axiom Math has announced that it has completed the computer verification of the classification of finite simple groups (CFSG), which mathematicians call the "Enormous Theorem." In 24 days, dozens of AI agents wrote about 43.1M lines of Lean code and formalized a proof that spans 15,000 pages across more than 500 research papers. About 100 researchers worked on that proof over several decades. Axiom calls the result the first complete computer-verifiable proof of CFSG. The code and materials have been published for independent review.

A periodic table of symmetries

The easiest way to see what the theorem classifies is a cube. You can rotate it in 24 ways so that it looks exactly the same. Those rotations form a mathematical group. CFSG describes the fundamental "building blocks" from which all finite symmetry groups are assembled. The result is a kind of periodic table of symmetries, used in algebra, number theory and mathematical physics.

The problem is how the proof was built. Different authors assembled it piece by piece, across hundreds of papers and several decades. For a single person, rechecking all of it is practically impossible: you would have to hold thousands of interlinked lemmas scattered across journals in your head. Formalization in Lean removes that obstacle. Every step of the reasoning is written as code, and the Lean kernel mechanically checks that each conclusion follows from the previous ones.

Project arithmetic: 43 million lines in 24 days

The numbers set the scale. 43.1M lines in 24 days works out to roughly 1.8M lines per day, or about 75,000 per hour around the clock. That is roughly 2,900 lines of formal code per page of the paper proof. Formalization is orders of magnitude more detailed than the original text, because mathematicians skip "obvious" steps in papers and Lean does not allow that.

This was agentic work, not one long generation. Dozens of agents ran parallel branches of the formalization, and the final code had to converge into a single proof that the checking kernel accepts. That kernel check is what separates this result from ordinary language-model output: an erroneous step simply does not pass.

What the agents found along the way

The formalization produced new findings as well as confirmation. Axiom lists these results:

• about 43.1M lines of Lean code, produced in 24 days by dozens of AI agents;
• 34 substantive discrepancies with published mathematical work;
• counterexamples to some statements in the literature, along with alternative proofs for them;
• a new result in group theory, needed for the chosen proof path;
• in some cases, errors found in the original reasoning, plus new mathematical arguments that correct them;
• joint work with mathematicians, including specialists who took part in the original classification.

Human involvement matters here. When a formalization runs into a discrepancy with a publication, an expert has to tell a typo from a real gap. The experience of the original classification's authors helped determine where the formal version should follow the original and where a different route was needed.

What practitioners can take from this

The main takeaway for the industry: agents that write and self-check code in an environment with a strict verifier can handle tasks that are out of reach for manual work. Lean acts as a judge that takes neither humans nor the model on faith. The same approach applies to any field where results can be checked automatically: verification of critical software, protocols and cryptographic constructions.

There is also a caveat. Computer verification guarantees that the proof is correct relative to the written definitions and statements. That is why the open code matters as much as the result itself: mathematicians can read the definitions and confirm that what was formalized is what was intended. Axiom's announcement does not give the cost of the run (compute and token spend). That figure will show whether formal rechecking of foundational results becomes routine or stays a one-off project.

For mathematicians, the signal is clear. Literature that once had to be accepted on trust in authority can now be fully rechecked mechanically, and 34 substantive discrepancies have already turned up along the way.