# Axiom's AI agent swarm formalizes the classification of finite simple groups in 24 days

> Original title: Verified AI just had its greatest month.

- Source: Rohan Paul
- Published: 2026-10-27T23:31:32.000Z
- Bad Influence: https://badinfluence.news/items/t4ck8e41nn45xzjhli6i7puyt
- Original: https://x.com/rohanpaul_ai/status/2115224910603890778

## Summary

Axiom's AI agent swarm turned 15,000 pages across more than 500 papers into over 38 million lines of machine-verified code in 24 days. The effort also uncovered 34 serious discrepancies in the published record. The post quotes @biosemiote, who calls the formal proof of CFSG possibly among the largest open-source projects ever and says the work reflects decades of human mathematics. The attached chart shows Axiom's CFSG effort at 43.0M Lean lines, compared with other Lean formalizations since June 2025.

## Post

Verified AI just had its greatest month.

A swarm of AI agents just did what no mathematician could do alone: check every step of the longest proof in history.

For 40+ years, mathematicians have built on the Classification of Finite Simple Groups without anyone being able to check it alone. 

Axiom’s AI agent swarm just did it in 24 days, turned 15,000 pages across 500+ papers into 38M+ lines of machine-verified code. And it also uncovered 34 serious discrepancies in the published record.

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

## Quoted post @biosemiote

> The formal proof of CFSG may now be among the largest open-source projects ever. Watching agents assemble it is a reminder of the awe-inspiring human achievement behind it. The graph represents some 15,000 pages of intricate arguments developed by mathematicians over decades.

https://x.com/biosemiote/status/2115215322362032163