Classification of Finite Simple Groups Formalized in Lean (cfsg.axiommath.ai)
205 points by pfdietz 16 hours ago
mlmonkey 16 hours ago
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 my understanding of Lean is wrong; I'm thinking of it as a programming language but for Math.
jonath_laurent 15 hours ago
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 incompatible ways.
petesergeant 2 hours ago
As someone with a highly uneven and kinda basic maths background, I'd have thought that simplification of a proof, and pulling things into a coherent whole would be exactly what computers excel at, but everything I've seen (or heard) suggests that's not really the case. Are you able to explain why?
fspeech an hour ago
whatshisface 7 hours ago
What were the agents based on?
hujun236 6 hours ago
When two sources formalized the same object in incompatible ways, did the swarm mostly emit translation lemmas between them, or did someone pick a canonical definition and have downstream proofs rewritten to match? The second feels like where the "coherent whole" cost actually sits, and I'm curious how much of the 500-source effort was that reconciliation versus line-by-line translation.
bananaflag 15 hours ago
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 months.
xelxebar 4 hours ago
The really interesting aspect of this, IMHO, is discovering what theorem formulations combine together well as a whole. It's much akin to a software architecture problem.
Metamath has done quite a bit or primary research into this. Theorems often have a slightly non-standard, but more general form.
One can ask things like, "what is the equivalent of functional programming?" Or, "is there global state?" It's a perspective on reverse mathematics.
thaumasiotes 14 hours ago
> Of course you can include two or five or ten equivalent formulations (like textbooks sometimes do) but still, not everything under the sun.
Note that mathlib currently includes duplicates of many theorems; I believe deduplication is an active goal (if not one seeing much labor right now).
aureianimus 14 hours ago
Yes and no. With enough compute, probably, but doing this does not necessarily yield a reusable library. See https://xenaproject.wordpress.com/2026/10/16/how-to-formaliz...
Someone 12 hours ago
_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.
tyromaniac 16 hours ago
Write a few proofs with it and then come back to this
QuesnayJr 15 hours ago
I think people assume that it would end up not being usable by humans without a lot of hand-holding. Though maybe that's wrong, and somebody should try it.
sebzim4500 16 hours ago
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 the future like we do in e.g. physics.
QuesnayJr 15 hours ago
They didn't discover a missing sporadic group. The big gap in the proof (the quasithin case) happened because it was covered in a 600-page unpublished manuscript that under further investigation turned out to be incomplete.
Davidzheng 9 hours ago
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.
m_j_g 9 hours ago
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 presentation: https://types2026.cse.chalmers.se/slides/51.pdf
abstractanimal 7 hours ago
Last week I blew my whole Claude Max weekly budget having Opus translate from Mathlib to Coq-HoTT. It was so beautiful I can't wait to do it again this week.
Ericson2314 4 hours ago
No Type Theory won: Per Martin-Löf is still alive and should be able to confirm his work lives in some form in Lean. Zermelo and Fraenkel would be utterly confused, however.
What you mean it say is that Lean is not a HoTT, and Mathlib has tons of classical reasoning (excluded middle, axiom of choice).
I don't think it's too late at all for HoTT. In fact, I think the AI companies will find trying to crank out more new math which is out of distribution in a funky way a highly useful exercise.
edflsafoiewq 4 hours ago
Why is that sad?
HappyPanacea 8 hours ago
The stronger AI become the easier it should be to develop and move to alternative foundations.
anon291 5 hours ago
Hey now... If you have a formulation in type theory (lean is not set theory), then you can translate to homotopy type theory fairly easily
compacct27 12 hours ago
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 up the field solo and see what it has to offer us
senderista 13 hours ago
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.
richard_chase 4 hours ago
I was thinking this would be done at some point but not so soon.
pfdietz 16 hours ago
The formalization is 43.1M lines of Lean.
bwestergard 15 hours ago
Is that going to be mathematically useful?
sebzim4500 15 hours ago
It's nice to know that they didn't miss anything. The natural language proof is 10,000 pages and they have missed groups in the past.
cvoss 10 hours ago
Panoramix 13 hours ago
pfdietz 14 hours ago
The proof was of such complexity and length there were lingering doubts. This dispels them.
curt15 15 hours ago
More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.
cubefox 13 hours ago
I suppose this is the longest Lean proof by a wide margin.
pfdietz 12 hours ago
It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux).
cubefox 11 hours ago
claudismusa 9 hours ago
I used to take mathematicians seriously.
gggg_g_g__g 10 hours ago
Holy shit.
vessenes 10 hours ago
Note they found one gap (and filled it) in the previously accepted 1,000+ page proof. So that's pretty cool.
sleepyams 10 hours ago
Somehow the classification of finite simple groups makes me feel uneasy as a mathematician, but I suppose this helps quell that feeling.
jbaber 9 hours ago
vatsachak 15 hours ago
LLM formalization is not as useful as human formalization, but nice to know that the Classification is correct
pixl97 16 hours ago
Page has some kind of redirect bug that steals the back button, may want to open it in a new tab to avoid that.
QuesnayJr 15 hours ago
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.
bamb008 14 hours ago
In [1] they claim:
>However, there were 34 noteworthy deviations from the published record that needed to be resolved, the most substantial of which related to the Unbalanced Group Theorem.
[1]https://axiommath.ai/research/the-enormous-theorem-formalize...
contubernio 15 hours ago
Many many gaps had been found and patched (by humans) already over the last forty years.
xiaodai 5 hours ago
what a monster of an effort!
sdenton4 2 hours ago
i_see_what_you_did_there.gif
esafak 12 hours ago
Looking at the visualizations made me wonder if the embeddings themselves can be used to suggest, if not derive, mathematical results. I realize it depends on the quality of the embeddings.
v3ai 15 hours ago
based if true