2.6K views · 10 likes · 1 reposts (at collection)
Axiom reports formalizing the Classification of Finite Simple Groups in Lean
- Who
- Axiom
- What
- announced a complete Lean formalization of the Classification of Finite Simple Groups
- When
What happened
Axiom says dozens of AI agents formalized the Classification of Finite Simple Groups in Lean in 24 days, covering about 15,000 pages across more than 500 papers. According to Baoyu’s account, the system found a flaw in John Walter’s 1986 proof and produced a replacement using Ronald Solomon’s 1976 approach. Axiom reports that all checks passed, but independent external verification has not been reported, and human review is needed to confirm that the formal statement matches the intended theorem.
Why it matters
The distinction between checking proof steps and checking the formal theorem statement clarifies which parts of Axiom’s reported formalization still depend on human review.
Read next
See the full storyAxiom Says AI Agents Completed Lean Formalization of the Classification of Finite Simple GroupsThe story so far
Axiom says dozens of AI agents completed a Lean formalization of the Classification of Finite Simple Groups in 24 days and that all checks passed. The claimed formalization covers a proof spanning about 15,000 pages across more than 500 papers. Human review is still needed to confirm that the formal statement matches the intended theorem. According to Baoyu’s account, Axiom’s system also found a flaw in John Walter’s 1986 proof and produced a replacement using Ronald Solomon’s 1976 approach.
Keep up with AI, one email a day
Model releases, price changes and compute developments, with original sources. Free, confirmed by email, and easy to unsubscribe. Read a past issue · 2026-10-27