Mathematicians Build Long-Awaited Graph Sandwich

4 comments

• mindleyhilner 2 hours ago
  Actual meat: https://arxiv.org/abs/2510.20765
  [-]
  • bananaflag 4 minutes ago
    Nice, it's pre-AI
  • emil-lp 51 minutes ago
    Isn't it actually the bread? The meat is given, if I understand correctly.
• Sniffnoy 36 minutes ago
  Wondering: if the process for the upper part of the sandwich is the complement of the process for the lower part, why was it so much more difficult? What would go wrong if you took one of the earlier lower-sandwich processes, and complemented it in a similar way? I have to assume it's something, but what?
• bhouston 2 hours 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 51 minutes ago
    No, almost none (except for in certain fields, such as HoTT) have formalized proofs.
  • danabramov 2 hours ago
    It's new but there is actually a registry now: https://palomar-registry.org/
  • UltraSane 2 hours 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 3 hours ago
  Seems like this would have strong implications for distillation and/or smaller types of transformers!
  [-]
  • emil-lp 50 minutes ago
    No, this is pure graph theory, and is quite far away from anything machine learning.
  • Scene_Cast2 2 hours ago
    How? I don't see it. (I'm familiar with the ML side, not the combinatorics side.)