Classification of Finite Simple Groups Formalized in Lean(cfsg.axiommath.ai)
111 pointsby pfdietz4 hours ago12 comments
  • compacct27a minute 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
  • mlmonkey4 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_laurent4 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.

    • bananaflag4 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.

      • thaumasiotes2 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).

    • aureianimus2 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...
    • 2 hours ago
      undefined
    • tyromaniac4 hours ago
      Write a few proofs with it and then come back to this
    • QuesnayJr3 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.
  • sebzim45004 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.

    • QuesnayJr3 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.
  • pfdietz4 hours ago
    The formalization is 43.1M lines of Lean.
    • bwestergard4 hours ago
      Is that going to be mathematically useful?
      • sebzim45003 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.
        • Panoramixan hour ago
          How do we know the formalization itself doesn't have any errors? AFAIK it's very far from trivial to formalize something.
          • sebzim4500an hour ago
            In general checking that the definitions are correct isn't that hard and assuming at least one of the lean kernels you verify with is correct (which tbf is an assumption, the implementations are based on each other so could have a common bug) that's all you need to verify.

            In this case the statement is unusually complicated but still much much easier to verify than the proof itself.

      • pfdietz2 hours ago
        The proof was of such complexity and length there were lingering doubts. This dispels them.
      • 3 hours ago
        undefined
      • curt153 hours ago
        More so if Lean uncovers logical errors. Note also there is already an ongoing 2nd generation proof.
    • cubefoxan hour ago
      I suppose this is the longest Lean proof by a wide margin.
      • pfdietza few seconds ago
        It's possibly the longest open source project of any kind (depending on whether you count comments and white space in Linux).
  • senderistaan hour 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.
  • vatsachak4 hours ago
    LLM formalization is not as useful as human formalization, but nice to know that the Classification is correct
  • QuesnayJr3 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.
  • esafak39 minutes 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.
  • pixl974 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.
  • an hour ago
    undefined
  • Salparvezml3 hours ago
    [flagged]
  • v3ai4 hours ago
    based if true