The formalization is 43.1M lines of Lean.

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.

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.

Page has some kind of redirect bug that steals the back button, may want to open it in a new tab to avoid that.

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

based if true