# Axiom formalizes the Classification of Finite Simple Groups in Lean in 24 days

> Original title: Big win for verifiable AI.

- Source: Rohan Paul
- Published: 2026-10-27T15:12:41.000Z
- Bad Influence: https://badinfluence.news/items/q7nmh7b4ihnras32mg8ii28c8
- Original: https://x.com/rohanpaul_ai/status/2115099371608137823

## Summary

Axiom has released a complete computer-checked Lean proof of the Classification of Finite Simple Groups, a roughly 15,000-page proof written by about 100 mathematicians. Over 24 days, engineers and mathematicians directed swarms of dozens of AI agents, which produced about 38 million lines of Lean code. Axiom credits the speed to rebuilding its models, harness and infrastructure together.

## Why it matters

The source gives concrete scale and timing for a formal proof effort, showing what AI agent swarms can produce under mathematician supervision.

## Post

Big win for verifiable AI.

Formal Math proof is starting to scale like software.

@axiommathai rewrote the longest proof in mathematics, all 15,000 pages, about 40 million lines of Lean. 
Swarms of AI agents wrote it in 24 days while mathematicians steered them.

Axiom says that at the start of this year, getting AxiomProver to write a correct 10,000-line Lean proof took weeks of coaxing. And now this swarm of agents formalized a problem roughly 4,000 times that size in 24 days.

The target was the Classification of Finite Simple Groups: about 15,000 pages, 500+ papers, around 100 authors, and no single reader who has gone through all of it.

Axiom credits the jump to rebuilding three layers at once: the models, the harness and the infrastructure.

![](https://badinfluence.news/api/img-proxy?u=https%3A%2F%2Fpbs.twimg.com%2Fmedia%2FHVpV1h_bsAE8n7V.jpg&mode=thumb&exp=1793404800&sig=972fd6ef76a4e29b)

## Quoted post @axiommathai

> The largest math proof in human history is now computer-verified.
> 
> Today, Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, the "periodic table of symmetry."
> 
> About 15,000 pages, built by over 100 mathematicians across generations.

https://x.com/axiommathai/status/2115089794867040584