4 ms·
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 chun
by cryptolobster 14d ago
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?
- minkowski 13d agoProbably not since LLMs can now carry out very large formalizations (https://www.anthropic.com/research/formalizing-fermats-last-theorem https://www.anthropic.com/research/formalizing-fermats-last-...).
- rbanffy 11d agoUnless 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.