Mathematicians Build Long-Awaited Graph Sandwich

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?

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?

Seems like this would have strong implications for distillation and/or smaller types of transformers!

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?

Hilarious - a mathematical result that afaict has nothing whatsoever to do with AI, and 75% of the comments are about AI, including this one!

Actual meat: https://arxiv.org/abs/2510.20765