Mathematicians Build Long-Awaited Graph Sandwich

3 comments

• mindleyhilner 2 hours ago
  Actual meat: https://arxiv.org/abs/2510.20765
  [-]
  • emil-lp 4 minutes ago
    Isn't it actually the bread? The meat is given, if I understand correctly.
• bhouston 1 hour ago
  I am not a mathematician but are most papers now accompanied by a lean proof?

  Is there a central repository of lean proofs shared by mathematicians like an npm repository of JavaScript packages?

  Does it all depend on a stupid is-odd package in the end?

  [-]
  • emil-lp 4 minutes ago
    No, almost none (except for in certain fields, such as HoTT) have formalized proofs.
  • danabramov 1 hour ago
    It's new but there is actually a registry now: https://palomar-registry.org/
  • UltraSane 1 hour ago
    LLMs have gotten good at creating Lean proofs so the are much more common but not universal. And they depend on https://github.com/leanprover-community/mathlib4
• NickNaraghi 2 hours ago
  Seems like this would have strong implications for distillation and/or smaller types of transformers!
  [-]
  • emil-lp 2 minutes ago
    No, this is pure graph theory, and is quite far away from anything machine learning.
  • Scene_Cast2 1 hour ago
    How? I don't see it. (I'm familiar with the ML side, not the combinatorics side.)