If it was in Lean anyone could verify it instantly. That is the huge advantage of it. Manual math Proof verification labor might be the most limited resource ever.
There can't be too many people working in that corner of graph theory, and I expect the result to them being eminently straightforward.