4 ms·
It did not use Lean or other proof assistant?
by azaras 3mo ago
It did not use Lean or other proof assistant?
- emil-lp 3mo agoThere'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.
- sigbottle 3mo agowhat kinds of proofs would it be good at? I thought that combinatorial proofs would be easier to reason over than ones that required analysis
- ComplexSystems 3mo agoHow many tokens would it cost to write some library functions to fill in the gaps?
- varjag 3mo agoYou could try solving that in Lean perhaps
- aureianimus 3mo agoGraphlib? Do you have a link to this for me?
- kzrdude 3mo agoI guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean https://github.com/openai/cdc-lean