[HN Gopher] Mathematicians Build Long-Awaited Graph Sandwich
___________________________________________________________________
Mathematicians Build Long-Awaited Graph Sandwich
https://arxiv.org/abs/2510.20765
Author : ibobev
Score : 76 points
Date : 2026-09-18 14:41 UTC (16 hours ago)
HTML web link (www.quantamagazine.org)
TEXT w3m dump (www.quantamagazine.org)
| NickNaraghi wrote:
| Seems like this would have strong implications for distillation
| and/or smaller types of transformers!
| Scene_Cast2 wrote:
| How? I don't see it. (I'm familiar with the ML side, not the
| combinatorics side.)
| emil-lp wrote:
| No, this is pure graph theory, and is quite far away from
| anything machine learning.
| mindleyhilner wrote:
| Actual meat: https://arxiv.org/abs/2510.20765
| emil-lp wrote:
| Isn't it actually the bread? The meat is given, if I understand
| correctly.
| bananaflag wrote:
| Nice, it's pre-AI
| bhouston wrote:
| 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?
| danabramov wrote:
| It's new but there is actually a registry now: https://palomar-
| registry.org/
| UltraSane wrote:
| 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
| emil-lp wrote:
| No, almost none (except for in certain fields, such as HoTT)
| have formalized proofs.
| bhouston wrote:
| Why not? It seems like this should sort of be the standard
| now? Or is it hard to make lean proofs in all fields?
| bbeonx wrote:
| i think there are a few reasons.
|
| - lean proofs are hard, and a lot of the time there is so
| much mathematical machinery that folks are working on that
| you would need to not only prove your result, but also all
| of the machinery that your subfield it is built on. it
| would be infeasible for many authors to do all of this work
| (this might be a major part of multiple careers, and when
| there are 5 folks in your entire subfield, the payoff is
| not really worth it)
|
| - human proofs are readable, and can illustrate concepts
| better than lean proofs. human proofs give insights into
| how to think about a type of problem, and this is often the
| most valuable part of a proof/result.
|
| - lean proofs are often very difficult to read; while they
| give you a "verified" check mark, they do not necessarily
| improve the bounds of human understanding if that makes
| sense.
| bhouston wrote:
| Thank you for the response.
| Sniffnoy wrote:
| 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?
| zem wrote:
| my guess is that they also had to prove that the complement
| process was mathematically sound
| omnicognate wrote:
| Hilarious - a mathematical result that afaict has nothing
| whatsoever to do with AI, and 75% of the comments are about AI,
| including this one!
| bbeonx wrote:
| lol yeah we're doomed
| upheaval7276 wrote:
| and this one
|
| edit: AI
| cryptolobster wrote:
| Given how much surrounding machinery the graph sandwich proof
| depends on, would it even be feasible to formalize it in Lean
| without first formalizing large chunks of random graph theory?
| And if not, does that mean results like this will stay out of
| reach for formal verification for the foreseeable future?
___________________________________________________________________
(page generated 2026-09-19 07:01 UTC)