# Axiom open-sources AI-written Lean formalization of the classification of finite simple groups

> Original title: Axiom released an open-source GitHub repo where dozens of AI agents turned a 15,000-page math proof into about 43 million lines of code i...

- Source: Testing Catalog
- Published: 2026-10-28T10:44:03.000Z
- Bad Influence: https://badinfluence.news/items/hcjtzmtvzqmkv2v2wkgkr239a
- Original: https://x.com/testingcatalog/status/2115394156054933618

## Summary

Axiom released an open-source GitHub repository in which dozens of AI agents turned a 15,000-page proof into about 43 million lines of Lean code in 24 days. The Classification of Finite Simple Groups took 100 mathematicians several decades to develop, and Lean code lets the full result be checked by running it. Axiom's chart estimates that AI-written Lean projects have roughly doubled every 37 days since mid-2025.

## Why it matters

The item reports a concrete scale benchmark for AI-written formal proofs, with a 24-day timeline and a growth-rate estimate that readers can compare against other Lean projects.

## Post

Axiom released an open-source GitHub repo where dozens of AI agents turned a 15,000-page math proof into about 43 million lines of code in 24 days.

The proof, known as the Classification of Finite Simple Groups, took 100 mathematicians several decades and lists every basic building block of symmetry in mathematics.

The code is written in Lean, a programming language that checks every step of a proof, allowing the whole result to be verified by running the code instead of rereading hundreds of papers.

Axiom's chart tracks how large AI-written Lean projects have grown since mid-2025, roughly doubling every 37 days by its estimate, with this project reaching 43 million lines.

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

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