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.

▲

ComplexSystems 5 hours ago | parent | next [-]

How many tokens would it cost to write some library functions to fill in the gaps?

	▲	varjag 4 hours ago \| parent [-]
		You could try solving that in Lean perhaps

▲

aureianimus 3 hours ago | parent | prev | next [-]

Graphlib? Do you have a link to this for me?

▲

sigbottle 5 hours ago | parent | prev [-]

what kinds of proofs would it be good at? I thought that combinatorial proofs would be easier to reason over than ones that required analysis