Imagine you have the world's most complicated IKEA manual — not for a bookshelf, but for a cathedral. The manual is 10,000 pages long, written by a hundred different authors over fifty years, in slightly different dialects, with no single person alive who has read every page. Now imagine you hire a tireless, literal-minded clerk to re-derive every instruction from first principles, flagging any step where the logic doesn't follow. That's what this project did to the Classification of Finite Simple Groups (CFSG), one of the most important and sprawling theorems in all of mathematics. The CFSG states that every finite simple group — the atoms of symmetry, the indivisible building blocks from which all finite groups are assembled — falls into exactly one of four families: cyclic groups of prime order, alternating groups, groups of Lie type, or one of 26 exceptional "sporadic" groups. The first-generation proof of this fact was assembled across thousands of journal pages by roughly a hundred mathematicians from the 1950s through the early 2000s. No single human has ever verified the entire thing. The proof's correctness has rested, uncomfortably, on a social process: peer review distributed across decades and hundreds of specialists. This project changes that. The team — led by principal investigator Letong Hong, with core contributors Dean Cureton, Vasily Ilin, Bhavik Mehta, and Niels Voss, plus about two dozen mathematical and engineering contributors — translated the entire first-generation proof into Lean, a proof assistant whose kernel mechanically checks every logical step. The result: 43.1 million lines of Lean code, 2.05 million declarations, drawing on 715 source papers and books, organized into 100 milestones. Every inference is now machine-verified. The project didn't just rubber-stamp the existing proof. Along the way, the team found an issue in a published argument for the Unbalanced Group Theorem — a non-trivial component of the classification. They developed an alternative route and formalized that instead. This is the formalization payoff that advocates have long promised: when you force every step through a proof kernel, latent errors in century-old arguments surface. The fact that such an error existed in a proof of this stature, uncaught for decades, is itself a significant finding about the reliability of purely human verification at scale. The engineering achievement is staggering in scope. 43.1 million lines of code is larger than most industrial software systems. The project synthesized 139 source works spanning from the 1870s to the present, each contributing formalized statements. The team mixed mathematical contributors (who understood the group theory) with engineering contributors (who understood Lean's type system and tactic framework), a division of labor that mirrors the original proof's collaborative structure but adds a new dimension: human-machine collaboration at the frontier of mathematical certainty. What makes this more than an exercise in translation is the infrastructure it creates. A fully formalized CFSG means that any future result depending on the classification — and thousands do, across algebra, combinatorics, geometry, and theoretical physics — can now invoke it as a verified lemma rather than a social contract. The Lean codebase is public on GitHub and accompanied by an interactive proof map. This is not a sealed artifact; it's a foundation other formalizers can build on. The broader significance is a proof of concept for formalization at the extreme end of mathematical complexity. If the CFSG — perhaps the single hardest target in all of mathematics for formalization — can be done, the implicit claim is that nothing is out of reach. The question shifts from "can we formalize X?" to "how long will it take and how many people do we need?" That reframing is the real milestone.
