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?
Unless humans understand them, can we trust such formalisations? We can prove the formalisation is correct, but we can't prove it accurately reflects what we are trying to prove.
Of course, one has to convince oneself the Lean theorem is defined correctly, but it will be orders of magnitude shorter than the proof. (In this case, one would also need to assume that probability theory, random graphs, etc. are defined correctly, but one would generally be happy to leave this to others.)
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?
What goes wrong is the accuracy guarantee. Complementing gives an upper graph, but the old guarantee doesn’t establish that it’s close enough to the target graph - which is what the theorem requires…
- 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.
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?
Probably not since LLMs can now carry out very large formalizations (https://www.anthropic.com/research/formalizing-fermats-last-...).
Unless humans understand them, can we trust such formalisations? We can prove the formalisation is correct, but we can't prove it accurately reflects what we are trying to prove.
Of course, one has to convince oneself the Lean theorem is defined correctly, but it will be orders of magnitude shorter than the proof. (In this case, one would also need to assume that probability theory, random graphs, etc. are defined correctly, but one would generally be happy to leave this to others.)
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?
What goes wrong is the accuracy guarantee. Complementing gives an upper graph, but the old guarantee doesn’t establish that it’s close enough to the target graph - which is what the theorem requires…
my guess is that they also had to prove that the complement process was mathematically sound
Seems like this would have strong implications for distillation and/or smaller types of transformers!
No, this is pure graph theory, and is quite far away from anything machine learning.
How? I don't see it. (I'm familiar with the ML side, not the combinatorics side.)
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?
It's new but there is actually a registry now: https://palomar-registry.org/
No, almost none (except for in certain fields, such as HoTT) have formalized proofs.
Why not? It seems like this should sort of be the standard now? Or is it hard to make lean proofs in all fields?
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.
Thank you for the response.
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
Hilarious - a mathematical result that afaict has nothing whatsoever to do with AI, and 75% of the comments are about AI, including this one!
lol yeah we're doomed
and this one
edit: AI
Actual meat: https://arxiv.org/abs/2510.20765
Isn't it actually the bread? The meat is given, if I understand correctly.
Nice, it's pre-AI