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.