← Back to context Comment by azaras 2 months ago It did not use Lean or other proof assistant? 6 comments azaras Reply emil-lp 2 months ago 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 2 months ago How many tokens would it cost to write some library functions to fill in the gaps? varjag 2 months ago You could try solving that in Lean perhaps sigbottle 2 months ago 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 2 months ago Graphlib? Do you have a link to this for me? kzrdude 2 months ago I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean
emil-lp 2 months ago 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 2 months ago How many tokens would it cost to write some library functions to fill in the gaps? varjag 2 months ago You could try solving that in Lean perhaps sigbottle 2 months ago 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 2 months ago Graphlib? Do you have a link to this for me?
ComplexSystems 2 months ago How many tokens would it cost to write some library functions to fill in the gaps? varjag 2 months ago You could try solving that in Lean perhaps
sigbottle 2 months ago 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
kzrdude 2 months ago I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean
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.
How many tokens would it cost to write some library functions to fill in the gaps?
You could try solving that in Lean perhaps
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
Graphlib? Do you have a link to this for me?
I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean