Hacker News new | ask | show | jobs
by emil-lp 22 days 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.
3 comments
ComplexSystems 22 days ago
How many tokens would it cost to write some library functions to fill in the gaps?
link
varjag 22 days ago
You could try solving that in Lean perhaps
link
sigbottle 22 days 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
link
aureianimus 22 days ago
Graphlib? Do you have a link to this for me?
link