# Axiom completes a Lean formalization of the Classification of Finite Simple Groups

> Original title: A bunch of agents chose which tasks to work on, wrote proofs, audited each other's work, and merged their contributions.

- Source: Santiago
- Published: 2026-10-27T14:43:00.000Z
- Bad Influence: https://badinfluence.news/items/guqe5udaozzaqjqim7o4918do
- Original: https://x.com/svpino/status/2115091901565313446

## Summary

Axiom announces a complete Lean auto-formalization of the Classification of Finite Simple Groups, about 15,000 pages built by more than 100 mathematicians across generations. The author says multiple agents chose tasks, wrote proofs, audited each other's work, and merged their contributions, and adds that agents may eventually work independently for long periods.

## Post

A bunch of agents chose which tasks to work on, wrote proofs, audited each other's work, and merged their contributions.

This is what software development will look like in the future. Heck, it's pretty much what it looks like right now!

It's hard to comprehend the scale we'll reach when agents can work independently indefinitely.

Read this below.

## 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