Axiom Says Its AI Formalized the 15,000-Page Classification of Finite Simple Groups in 24 Days: Claimed vs Verified

Axiom, the AI math startup behind AxiomProver, announced that its agents completed a full Lean formalization of the Classification of Finite Simple Groups, a proof of about 15,000 pages, in 24 days. If it holds up, it is one of the largest machine-checked mathematics projects ever attempted. As of this writing, though, we found the announcement and a secondary report, but no public repository or paper to check. This post separates what is claimed from what is verified.

TL;DR: claimed vs verified

What is the theorem, and why is it hard?

The Classification of Finite Simple Groups sorts every finite simple group, the indivisible building blocks of finite symmetry, into a short list: cyclic groups of prime order, alternating groups, 16 families of Lie-type groups, and 26 sporadic groups. The proof is not one paper. It is a body of work spanning decades, by more than 100 mathematicians and over 500 papers according to the coverage, and it is famously difficult to audit as a whole. That is exactly why a formal, machine-checked version would matter: Lean either accepts every step or it does not.

Formalizing something this big is not a matter of typing the existing text into Lean. Informal proofs skip steps that experts fill in silently. A formalizer has to supply them, and sometimes discovers the original gap was real.

What Axiom actually said

Per the post on X from @axiommathai as summarized by the aggregator pages we could read, Axiom described a complete Lean auto-formalization of the proof, calling it the "periodic table of symmetry," and said its agents, working with human guidance, converted the document into a chain of checkable logical steps and repaired errors found in the original text. The post is dated October 27, 2026; a Cryptobriefing report dated October 26 says Axiom announced it that day. The one-day gap is probably time zones, but it is a reminder that we are reconstructing the timeline from secondary pages.

What the secondary report adds, and why to be careful

The Cryptobriefing article quotes Axiom as saying AxiomProver produced "the first full computer-checked formalization" of the classification, and adds numbers: about 43.1 million lines of Lean, described as the largest Lean codebase ever created, over 2,000 errors or gaps found in the literature (34 classified as notable deviations), and a significant gap in the Unbalanced Group Theorem that needed a new proof segment. It names Axiom's founding CEO Carina Hong and mathematician Ken Ono as connected to the effort.

Our fetch of that article found no link to an Axiom document, repository, paper or Lean code. It attributes the numbers to unnamed "research findings," and says review was "overseen by expert mathematicians" without naming any. That does not mean the numbers are wrong. It means we cannot confirm them, and so neither can you from that article alone. A crypto-news outlet is also not where we would expect a first report of a mathematics milestone, which is another reason to wait for the primary document.

A formal verification seal at the center of a puzzle, illustrating Lean auto-formalization of a mathematical proof

Why Lean makes this checkable, in principle

Lean is a proof assistant: a proof is code, and a small trusted kernel checks every inference. That gives this kind of claim an unusual property. Unlike a benchmark score, a Lean formalization can be re-checked by anyone who has the files. If Axiom publishes the repository, the "does it compile" question is answered in hours on enough hardware, and the line count is just a wc.

Two things Lean does not settle:

1. Statement fidelity. The kernel guarantees the formal theorem is proved, not that the formal statement means the same as the classical theorem. Definitions of "finite simple group," "sporadic group" and the final classification statement must be reviewed by humans. Missing or weakened definitions are the classic way a formal proof can be technically correct and mathematically hollow.
2. Trusted assumptions. Any added axioms, or use of unverified automation, must be disclosed. A clean build with no extra axioms is the bar.

We have covered this distinction before. See how Anthropic's Claude Lean proof of Fermat's Last Theorem was framed, the claimed-vs-verified read on OpenAI's integer multiplication Lean proof, and the 3SUM/APSP claim and what is verified. The same questions apply here: where is the repo, who reviewed the statements, and what was human-written?

What we know about Axiom's track record

Axiom Math is an AI lab focused on formal proofs in Lean. Its X account says AxiomProver has produced 25 million lines of Lean (a post dated October 13) and ranked first on the Annals Bench (October 15), both self-reported by Axiom. Those are Axiom's own statements, not independent measurements. A track record on benchmarks and competition-style problems is relevant but not proof that the system scales to a 43-million-line project.

The size claim in context

If the 43.1 million line figure is right, it dwarfs the projects most people associate with large Lean efforts. Our own earlier reporting on the falling price of formal proof, in Lean 4 and the formal proof cost collapse, argued that agents make formalization dramatically cheaper. A 24-day timeline for work that human teams spent decades on would be the strongest data point yet for that thesis, which is exactly why it deserves a high bar of evidence. We could not find the build logs, compute cost, or the human effort behind "human guidance," and each changes the interpretation. Twenty-four days of agents with ten mathematicians steering is a very different result from twenty-four days with one.

How to check the claim yourself

1. Find the primary announcement. Open the @axiommathai post and any linked Axiom blog or paper. Note what it says exactly, including whether the claim is "complete," "full" or "of the main theorem."
2. Look for a public repository. A GitHub or Lean community link with a build instruction is the real deliverable. No repo means no verification.
3. Check axioms. Run #print axioms on the main theorem. Only the standard Lean axioms should appear; anything else must be explained.
4. Read the definitions. Ask a group theorist, or a Lean community member, whether the formal definitions match the classical ones.
5. Look for independent confirmation. Reactions from named mathematicians and Lean maintainers are the tiebreaker. Our roundup of expert reactions to AI math results shows how quickly those arrive when a claim is real, and how they sound when it is not.

Why it matters if it holds

The classification is a case where trust in the literature has been a live concern: parts of the proof were long considered incomplete and were patched by later work. A machine-checked version would turn a social consensus into a mechanical certificate, and a reported 2,000 errors, if real and mostly minor, would be a useful measure of how much of a human-written megaproof is held together by expert intuition. It would also push mathematics toward the position the Physical Superintelligence Lean proofs coverage described: results come with a checkable artifact or they do not count.

For people who build with AI, the practical lesson is about evaluation, not group theory. The most trustworthy AI results are the ones with a verifier attached: a compiler, a test suite or a proof kernel. This claim is attractive because it can be checked, and the right response is to ask for the thing that lets us check it.

What we will watch for

• An Axiom blog post, paper or repository with the full Lean source.
• Named independent reviewers, including group theorists and Lean maintainers.
• Axiom's account of what "human guidance" meant, and the compute used.
• Confirmation or correction of the 43.1 million line, 2,000 error and Unbalanced Group Theorem figures.

None of these requires special access. If Axiom publishes a repository, a reader with a Lean toolchain and enough compute can rebuild it and read the headline theorem statement directly. Until then, the sensible reading is that this is a credible-sounding announcement from a company with a self-reported track record, with the most dramatic numbers resting on one secondary source.

We will update this post when any of them lands.

Related reading

• Claude's Lean proof of Fermat's Last Theorem
• OpenAI integer multiplication Lean proof: claimed vs verified
• Claude 3SUM/APSP claim: what is verified
• Lean 4 and the formal proof cost collapse
• Physical Superintelligence: five open problems, Lean proofs, claimed vs verified
• OpenAI math results that matter: expert reactions
• External: Axiom on X Details reflect public information available on October 27, 2026 and will change as Axiom publishes more.