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?