HN

Comments (59)

• pred_
  What did it cost and how much energy was spent?
• Menu

  mlmonkey
  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.
• Menu

  sebzim4500
  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.
• Menu

  Davidzheng
  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.
• compacct27
  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
• gdiamos
  This tech is about to come for software.
• senderista
  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.
• Menu

  pfdietz
  The formalization is 43.1M lines of Lean.
• richard_chase
  I was thinking this would be done at some point but not so soon.
• vessenes
  Note they found one gap (and filled it) in the previously accepted 1,000+ page proof. So that's pretty cool.
• Menu

  sleepyams
  Somehow the classification of finite simple groups makes me feel uneasy as a mathematician, but I suppose this helps quell that feeling.https://en.wikipedia.org/wiki/Monster_group
• vatsachak
  LLM formalization is not as useful as human formalization, but nice to know that the Classification is correct
• pixl97
  Page has some kind of redirect bug that steals the back button, may want to open it in a new tab to avoid that.
• Menu

  QuesnayJr
  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.
• anon
  undefined
• Menu

  xiaodai
  what a monster of an effort!
• esafak
  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.
• anon
  undefined
• Salparvezml
  [flagged]
• v3ai
  based if true