There's really no good proof system mature enough to do advanced graph theory. The leading library in Lean is Graphlib, and it's really not ready for research level theorems.

I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean