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/