Classification of Finite Simple Groups Formalized in Lean

Posted by pfdietz 1 hour ago

Counter36Comment16OpenOriginal

Comments

Comment by mlmonkey 1 hour 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.

Comment by jonath_laurent 48 minutes 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.

Comment by bananaflag 48 minutes 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.

Comment by QuesnayJr 12 minutes 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.

Comment by tyromaniac 53 minutes ago

Write a few proofs with it and then come back to this

Comment by sebzim4500 1 hour 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.

Comment by QuesnayJr 8 minutes 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.

Comment by vatsachak 51 minutes ago

LLM formalization is not as useful as human formalization, but nice to know that the Classification is correct

Comment by pfdietz 1 hour ago

The formalization is 43.1M lines of Lean.

Comment by bwestergard 48 minutes ago

Is that going to be mathematically useful?

Comment by sebzim4500 24 minutes 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.

Comment by curt15 21 minutes ago

More so if Lean uncovers logical errors. Note also there are already 2nd and 3rd generation proofs.

Comment by pixl97 1 hour 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.

Comment by QuesnayJr 14 minutes 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.

Comment by contubernio 1 minute ago

Many many gaps had been found and patched (by humans) already over the last forty years.

Comment by v3ai 33 minutes ago

based if true

Comment by Salparvezml 21 minutes ago

[flagged]