‘The largest proof in history, now computer-verified’: what Axiom’s AI and Lean actually prove

Short answer: according to Axiom, its AI agent system (AxiomProver) produced a complete Lean proof of the Classification of Finite Simple Groups (CFSG) in 24 days. CFSG is one of the longest theorems in mathematics. The code is public, and according to its README it is sorry-free and relies only on Lean’s three standard axioms. Two things are still missing: someone outside Axiom rebuilding the proof, and group theorists confirming that the Lean statement says what the theorem says. Lean vouches for the steps. Humans still have to vouch for the statement.

On Tuesday, October 27, at 11:34 Argentina time (14:34 UTC), Axiom’s official X account posted: "The largest math proof in human history is now computer-verified." The public repository went up the same morning, and the company’s blog walked through how it was done in unusual detail.

If you build with coding agents, the reason to care isn’t the math. This is the largest case so far of agents producing work that a machine can check without trusting them. The same idea applies to the code those agents write in your repo.

Below: what’s backed by evidence vs. what’s only claimed, what Lean checks and what it leaves to you, and a practical section on trying Lean and where formal verification pays off today.

What Axiom says, per its blog and repo

In plain terms, the theorem says every finite simple group belongs to one of the known families or is one of 26 sporadic groups, the largest being the Monster. Per Axiom’s blog, the original proof spans about 15,000 pages across more than 500 articles by roughly 100 mathematicians. According to Axiom, no single person has read all of it.

According to the same post:

• Over 24 days, Axiom’s engineers and mathematicians directed "swarms of dozens of AI agents" that produced approximately 43.1 million lines of Lean.
• Work started on October 1 with a Slack channel and a proof map built from the published literature, split into 108 milestones and about 380 smaller tasks. Agents claimed tasks and reported progress through GitHub issues and Slack.
• The proof builds on Mathlib and incorporates about 1.2 million lines from the Qiuzhen-CFSG project.
• Translating the literature into Lean surfaced problems: mostly minor (typos, table errors, dropped hypotheses), plus "34 noteworthy deviations from the published record" that had to be resolved.

Per the repository README, the proof is "sorry-free," targets Lean 4 v4.35.0-rc3, builds on Mathlib and TauCeti, and uses only the standard axioms Classical.choice, propext and Quot.sound, with no native_decide. Axiom didn’t write the top-level statement; it comes from the TauCeti project. The license is Apache 2.0.

The project site lists 43.1 million lines, 2.05 million declarations, and "every logical step checked by Lean’s kernel."

### Now the caveats, and they matter

The numbers don’t line up. The official X thread says "50 million lines of Lean" and that the AI "fixed hundreds of major errata". The blog says 43.1 million and 34 noteworthy deviations. I go with the blog and repo figures here because they’re more precise.

No outside check yet. As of writing, I couldn’t find an independent rebuild of the proof or any statement from the Lean FRO or Mathlib maintainers. Axiom itself asks group theorists and the Lean community to "rerun the proof check, and confirm that the Lean statement says what CFSG says." That’s the right ask, and it also tells you the step hasn’t happened.

Reproducing it is expensive. Per the README, a full lake build took them close to 24 hours, and that was with open Lake changes they plan to upstream. This isn’t an afternoon job on a laptop.

Many of the loudest voices are affiliated. Several of the most enthusiastic posts come from people who work at or with Axiom. The errata list, per the blog, will be released later in consultation with experts.

Status: public and checkable in principle; external validation pending.

The twist: the AI found a hole in a published argument

The size isn’t the interesting part. Per the blog and the accompanying paper, the agents found counterexamples to a claim used in a 1986 published route to the Unbalanced Group Theorem (UGT), a load-bearing piece of the first-generation proof.

The theorem survives. The paper is explicit that the obstruction concerns that particular argument, and that UGT has other proofs. To close the gap, per Axiom, AxiomProver proved a new result built on Ronald Solomon’s 1976 theory of maximal 2-components.

Another example from the blog: in Aschbacher and Smith’s "quasithin" volumes, a lemma asserted two quantities were equal. The agents found a counterexample using SL₂(5), where one is 1 and the other 2. Swapping equality for an inequality fixed the lemma, but later arguments that leaned on equality had to be revisited.

For developers, the takeaway is blunt: a strict checker doesn’t just confirm, it surfaces bugs that decades of human review missed, and it does so without trusting whoever wrote the code, human or agent.

One detail from the blog deserves a second read. Early on, some "manageable" milestones hid huge prerequisites that the agents had assumed rather than proved. Axiom deleted tens of thousands of lines built on those assumptions. The blog also notes Lean will happily accept a result proved under an extra, unproved assumption, so reviewers had to compare each proved statement against the real target. If you’ve ever watched an agent "make the tests pass" by editing the test, you know this failure mode.

The receipts

| When | Who | What happened | Outcome | |---|---|---|---| | 1976 | Ronald Solomon | Theory of maximal 2-components | Basis for the new result, per the paper | | 1986 | Walter | Publishes a route to UGT | Axiom finds counterexamples to one step, per its blog | | 2004 | Aschbacher & Smith | 1,221-page quasithin treatment | Closes the first-generation proof, per the blog | | Aug 11, 2026 | Nie, Zhang, Tang, Testa, Yau | FormaTheoria paper on arXiv | Prior work toward formalizing CFSG | | Oct 1, 2026 | Axiom | Opens the project channel | 108 milestones, ~380 tasks, per the blog | | Oct 10, 2026 | Axiom’s agents | "WE PROVED MONSTER IS SIMPLE" | Intermediate milestone, per the blog | | Oct 26, 2026 | Axiom | "Formalizing the Enormous Theorem" post dated | Official account of the process | | Oct 27, 2026, 10:19 ART | Axiom | Public GitHub repo created | Code under Apache 2.0 | | Oct 27, 2026, 11:34 ART | @axiommathai | Announcement thread on X | 100k+ impressions within hours |

Proven vs claimed vs rumor

| Claim | Status | Why | |---|---|---| | A public repo with the Lean proof exists | Proven | It’s on GitHub under Apache 2.0 | | No sorry, no extra axioms | Claimed | Stated in the README; the repo ships a comparator config allowing only the three standard axioms, but no external rebuild found | | ~43.1M lines in 24 days | Claimed | Per Axiom’s blog and site | | "50 million lines" | Claimed, inconsistent | From the X thread; doesn’t match the blog | | 34 noteworthy deviations from the literature | Claimed | Per the blog; the errata list isn’t out yet | | "Hundreds of major errata" | Claimed, inconsistent | From the X thread; the blog says 34 noteworthy plus many minor | | Counterexamples to a step in the 1986 UGT route | Claimed, detailed | Laid out in Axiom’s paper; awaiting third-party review | | The Lean statement faithfully captures CFSG | Pending | Axiom itself is asking experts to confirm | | "2,000+ mistakes found" | Rumor | From a post on X with no source; not in the blog | | "Settled beyond a doubt" | Overclaim | Wording from a post on X; external validation hasn’t happened |

What Lean checks, and what it doesn’t

Lean’s official reference has a whole page on this: Validating a Lean Proof. Read it end to end. Here’s the gist.

What Lean does check. The kernel accepts a proof only if every step follows from the available definitions, theorems and axioms. #print axioms shows what a theorem ultimately depends on. If you see sorryAx, something is unproved. If you see anything beyond propext, Classical.choice and Quot.sound, the theorem only holds if that extra axiom does.

What Lean doesn’t check. Whether the statement means what you think it means. The docs draw the line explicitly between "does the theorem have a valid proof" and "what does the theorem statement mean." Axiom’s blog says the same thing: humans inspect the statement and its definitions, Lean checks the deductions.

One line worth remembering. For verification purposes, the same docs put "un-reviewed AI-generated proofs and programs" in the potentially malicious bucket. That isn’t a dig at AI. It’s the right default for any code whose intent you haven’t confirmed. For that tier, the docs recommend lean4checker, which replays proofs through the kernel, and comparator, which builds the proof in a sandbox and checks that the proved theorem matches a trusted statement written separately.

Axiom’s repo ships a comparator.json with a challenge module, a solution module and the permitted-axioms list. That’s the right shape for third-party validation. Someone actually running it independently and publishing the result is a separate milestone, and I haven’t seen it yet.

What it means for agent-written code

The pattern carries over to software surprisingly well:

1. Agents perform where they can check themselves. In formal math the checker is Lean, and it doesn’t negotiate. In your repo the closest equivalents are the compiler, the type system, tests and static analysis. The stricter the checker, the more you can delegate.
2. The bottleneck moves to the spec. If the agent writes both the code and the test, the test can be as weak as the code. Lean has the same problem: a badly stated theorem can be proved perfectly and mean nothing.
3. Assumptions are the silent failure mode. Axiom’s agents assumed prerequisites instead of proving them. In software that’s the mock that always returns success, the TODO that never leaves, the // @ts-ignore. Hunt for them the way #print axioms hunts for sorryAx.
4. Scale costs infrastructure. Axiom had to distribute cached build results across machines and push heavy finite computations into separately checkable certificates. Put enough agents on one codebase and your CI becomes the bottleneck.

Checklist: try Lean and use formal verification today

1. Install Lean. The official install page recommends VS Code plus the official Lean 4 extension, which walks you through the rest. To just poke around, Lean in the browser needs no install.

2. Create a project and build it. With Lean installed (the version manager is elan):

bash lake new demo cd demo lake build

For projects that depend on Mathlib, follow the community guide.

3. Prove something and ask what it depends on.

```lean theorem add_comm' (a b : Nat) : a + b = b + a := by omega

#print axioms add_comm' -- On Lean 4.35.0 this prints: -- 'add_comm'' depends on axioms: [propext, Quot.sound] ```

4. See what an unfinished proof looks like.

```lean theorem todo (n : Nat) : n * 0 = 0 := by sorry

#print axioms todo -- Lean warns that the declaration uses 'sorry' -- and the axiom list includes sorryAx ```

5. Watch a weak spec get proved anyway.

```lean -- "The output is sorted" isn't enough: -- a function that always returns [] satisfies it. def mySort (_xs : List Nat) : List Nat := []

theorem mySort_sorted (xs : List Nat) : (mySort xs).Pairwise (· ≤ ·) := by simp [mySort] ```

The proof is valid and the function is useless. The missing piece is requiring the output to be a permutation of the input. That’s the review Axiom is asking for on the CFSG statement, in miniature.

6. Put it in CI. Lean’s docs recommend running lean4checker in CI and note the lean-action GitHub Action enables it with lean4checker: true. If you accept proofs written by an agent, write the statement yourself in a separate file and use comparator to check the proof against it.

7. Pick your battles. Formal verification pays off on small, critical pieces: parsers and serializers, authorization rules, money calculations, algorithms with clear invariants, protocols. For a settings screen, ordinary tests are still the cheaper tool.

8. Learn from official material. Theorem Proving in Lean 4 covers axioms, and Functional Programming in Lean teaches Lean as a programming language. Per Lean on X, there’s a Software Verification in Lean event at Stanford on November 7, co-organized by the Beneficial AI Foundation and the Lean FRO.

Bottom line

Axiom shipped something you can check, which already sets it apart from most AI announcements. The repo exists, the scaffolding for independent validation is there, and the write-up is detailed enough to admit its own dead ends. What’s missing is outside confirmation: nobody outside Axiom has publicly rebuilt the proof, the errata list isn’t out, and the X thread’s numbers don’t match the blog’s.

For anyone building with agents, the lesson holds either way: an agent is only as trustworthy as the checker in front of it and the spec you check it against. Lean sets the first bar very high. The second one is still your job.

FAQ

What did Axiom announce on October 27, 2026? Per its blog and official X account, a complete Lean proof of the Classification of Finite Simple Groups, produced in 24 days by swarms of AI agents directed by its team, totaling about 43.1 million lines of code.

Has it been independently verified? As of writing, I found no public third-party rebuild and no statement from the Lean FRO or Mathlib. Axiom has invited the community to do it.

What exactly does Lean guarantee? That every step of the proof follows from the declared definitions and axioms. It doesn’t guarantee the formal statement says what was intended; humans review that.

Did the AI find errors in the original proof? According to Axiom, yes: 34 noteworthy deviations and counterexamples to a step in a 1986 published route to the Unbalanced Group Theorem. The theorem still holds, and Axiom says it proved a new result to replace that step.

Is it 43 million lines or 50 million? The blog and project site say about 43.1 million; the X thread says 50 million. The blog figure is the more precise one.

Can I run the check myself? The code is public, but per the README a full build took close to 24 hours with Lake changes that aren’t upstream yet. To learn, start with a small project and #print axioms.

Is formal verification useful for production code? Yes, for small, critical pieces where you can write a clear spec. Elsewhere, the compiler, types and tests give you a better cost-benefit ratio.

Sources

• Axiom: Formalizing the Enormous Theorem (blog, Oct 26, 2026)
• Axiom CFSG project site
• AxiomMath/CFSG repository on GitHub
• CFSG statement in the TauCeti project
• Axiom paper: The Unbalanced Group Theorem (Hexagon)
• Axiom announcement thread on X
• Axiom on X: 50 million lines in 24 days
• Axiom on X: the Unbalanced Group Theorem
• Axiom on X: invitation to validate the proof
• Lean: Validating a Lean Proof
• Lean: install
• Lean in the browser
• Theorem Proving in Lean 4: axioms and computation
• Functional Programming in Lean
• Lean community and Mathlib: creating a project
• FormaTheoria on arXiv (Aug 2026)
• Lean on X: Software Verification in Lean at Stanford