[azaras]

It did not use Lean or other proof assistant?

[emil-lp]

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]

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

[varjag]

You could try solving that in Lean perhaps

[sigbottle]

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

[aureianimus]

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

[kzrdude]

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