Finite Simple Groups Classification Formalized in Lean, Gaps Found
A complete formalization of one of mathematics' greatest proofs uncovers errors in the original literature.
What to know
- A complete formal proof in Lean of the classification of finite simple groups—a landmark 1,000+ page proof by ~100 mathematicians over decades—has been released with every step verified by Lean's kernel.
- The formalization process discovered a gap in the published proof of the Unbalanced Group Theorem; researchers developed an alternative argument and are compiling errata with mathematicians.
- The project used AI agents to extract and integrate formalization from over 500 sources, facing challenges in reconciling multiple formalizations of the same informal concepts.
The dispute Whether complete automated formalization of all mathematical literature is practical given the combinatorial explosion of equivalent formalizations for the same concepts, or whether curated human-guided assembly is necessary. · positions read across 17 posts and comments
This is valuable work filling documented gaps, showing what AI should be used for rather than rushing novel research.
-
“Note they found one gap (and filled it) in the previously accepted 1,000+ page proof. So that's pretty cool.”
vessenes · Hacker News ↗
Formalization at scale faces real challenges in reconciling multiple ways of expressing the same mathematical concepts.
-
“One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but incompatible ways.”
jonath_laurent · Hacker News ↗
Large-scale automated formalization of all math textbooks may be feasible with frontier models but remains uncertain in practice.
-
“Out of curiosity: is it possible to take a frontier model and just let it loose on all math textbooks out there, converting each and every proof/theorem/lemma/etc. into Lean?”
mlmonkey · Hacker News ↗
Dean Cureton Core contributor to Lean formalizationVasily Ilin Core contributor to Lean formalizationBhavik Mehta Core contributor to Lean formalizationNiels Voss Core contributor to Lean formalizationAxiom MTS Organization leading the formalization project
How it unfolded 2 developments, newest first · click a bar or a number to jump articlespostscomments
-
2
Researcher describes use of swarm of AI agents to assemble formalization from 500+ sources
Jonath Laurent from Axiom MTS explains that the formalization was approached using agents tasked with processing sources scattered across more than 500 articles and books. A key challenge was assembling everything into a coherent whole, since the same informal concept can be formalized in slightly different but incompatible ways.
“What you describe is pretty close to how we formalised this proof, which is scattered across more than 500 articles and books: a swarm of agents was tasked with going through all these sources.”
— jonath_laurent -
we are moving forward steadily :) https://github.com/marcinjangrzybowski/cubical-bis/blob/inte... (see table in the middle of doc) mind, that it is fully constructive implementation, you can get arbitrary precision aproximation to every real expression. for now WIP, but soon will be aviable in cubical-library :) also our related TYPES2026…
2 more of the top 3 · 15 posts in this stretch
-
_If_ you have formalized a provable theorem in Lean, a simple bread-first search can prove it. It will take lots (and lots, and lots, and lots…) of time, though (https://en.wikipedia.org/wiki/General_Problem_Solver).LLMs can do smarter searches, and will likely find proofs for most of them, but are not guaranteed to find a proof.
-
Groups were my gateway drug into abstract algebra. A friend clued me into symmetry being everywhere and Groups are how symmetry is formalized, and it’s been a crazy journey understanding all that. The frontier models can tie those abstract concepts to plain English examples and answer questions decently well, it’s never been a better time to pick…
-
-
1
Formalization process uncovers error in published Unbalanced Group Theorem proof
While formalizing the first-generation proof, the team found counterexamples to a closure assertion used in a published route to the Unbalanced Group Theorem. They developed an alternative argument using Solomon's 1976 theory of maximal 2-components, with Theorem 2.3 on preservation of simple tops as the key step.
“While formalizing the first-generation proof, we found counterexamples to a closure assertion used in a published route to the Unbalanced Group Theorem.”
— Axiom MTS / cfsg.axiommath.ai -
Out of curiosity: is it possible to take a frontier model and just let it loose on all math textbooks out there, converting each and every proof/theorem/lemma/etc. into Lean? A frontier model should be able to do that, right? And it's a one-time task: do it once and it's there for eternity, available as a library to be used in other proofs.Maybe…
1 more of the top 2 · 2 posts in this stretch
-
This seems like a very good use of auto-formalization, because in the past mathematicians have incorrectly believed that they were finished with the classification only discover a missing class/sporadic group.The original proof was a collaboration of ~100 mathematicians, if Tao is correct then we should expect to see more such collaborations in…
-
-
background
Complete Lean formalization of finite simple groups classification released — A team led by Dean Cureton, Vasily Ilin, Bhavik Mehta, and Niels Voss, with 26 other contributors, publicly releases a fully formalized Lean proof of the classification of finite simple groups. Every logical step is checked by Lean's kernel, covering all cases: cyclic of prime order, alternating, Lie type, and 26 sporadic groups.
What people are saying 12 voices from 1 site · best of 17 · verbatim
- Can frontier AI models realistically formalize all mathematics textbooks at scale, or does the problem of multiple incompatible formalizations of the same concept make this intractable?
- How many other gaps or errors might exist in other major formalized proofs?
- Oct 28
-
I’m not sure what axiom maths business model is, seems like excesses of AI boom era.No one’s gonna care for formalizing a 10,000 page math proof with 46M lines of Lean code, unless it is very cheap to do, which seems unlikely.
-
Simplifying and composing these proofs with other proofs should probably be the next goal. And formalizing within other computational proof paradigms.
-
This is phenomenal, super important for me. I have always had my concerns about the classification, and the verification that such a monumental proof is correct gives me great confidence about the way we have been doing mathematics so far.
- Oct 27
-
The stronger AI become the easier it should be to develop and move to alternative foundations.
-
Makes me sad that the homotopical foundation people never got their shit together and now formalization is so mature but it's still done in set theoretic foundations.
-
Note they found one gap (and filled it) in the previously accepted 1,000+ page proof. So that's pretty cool.
-
Somehow the classification of finite simple groups makes me feel uneasy as a mathematician, but I suppose this helps quell that feeling.
-
Filling in well-known gaps like this is the kind of thing the AI companies should be doing, not trying to scoop research in progress.
-
Yes and no. With enough compute, probably, but doing this does not necessarily yield a reusable library. See
-
I'm surprised they only found one gap. I would have expected multiple (fixable) gaps would have been uncovered, especially since the result was spread over many papers by many different people.
-
Axiom MTS here. What you describe is pretty close to how we formalised this proof, which is scattered across more than 500 articles and books: a swarm of agents was tasked with going through all these sources.One challenge is assembling everything into a coherent whole, since the same informal concept can be formalised in slightly different but…
-
Yes, but thing is, for a lot of basic stuff there are myriad ways in which it is formulated, so humans have to decide which of them goes in the library. Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.Probably this will be done in some form in the coming…