Finite Simple Groups formalized in Lean
The gist
AI math startup Axiom announced a complete Lean proof of the Classification of Finite Simple Groups, built by AI agent swarms in 24 days.
The original proof spans about 15,000 pages and no one person has read it all.
How it unfolded
- Oct 1, 2026The team opened a Slack channel; a proof map assembled from published literature and earlier Lean work divided the job into 108 milestones and about 380 smaller tasks.
- Oct 2, 2026The first swarm went live; agents claimed milestones through GitHub issues, lead agents broke up hard arguments and reviewed statements, and others wrote Lean.
- Oct 10, 2026A message in the project's channel read: we proved Monster is simple.