# Axiom completes a full Lean formalization of the classification of finite simple groups

> Original title: Slowly, then all at once. A full Lean formalization of the classification of finite simple groups!

- Source: Kevin Weil
- Published: 2026-10-27T14:47:46.000Z
- Bad Influence: https://badinfluence.news/items/ov5z0bamyqav2us2dxhenmidq
- Original: https://x.com/kevinweil/status/2115093099114545488

## Summary

Kevin Weil says a full Lean formalization of the classification of finite simple groups is complete. He notes the original proof ran about 15,000 pages across 500 papers by 100 mathematicians, and says the formal version settles the result beyond doubt. The linked page on axiommath.ai describes the formalization.

## Post

Slowly, then all at once. A full Lean formalization of the classification of finite simple groups! 

The original proof was 15,000 pages of painstaking work across 500 papers by 100 mathematicians. Now settled beyond a doubt.

https://axiommath.ai/research/the-enormous-theorem-formalized/