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 (<a href="https://www.anthropic.com/research/formalizing-fermats-last-theorem" rel="nofollow">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.)
cryptolobster · · focus · HN ↗
minkowski · · focus · HN ↗
rbanffy · · focus · HN ↗
minkowski · · focus · HN ↗