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.