What might be the best software for checking the validity of proofs of graph theoretical statements? Lean, HOL, ... ? One criterion would also be, what would be the easiest for a graph theorist to learn and use, and what would allow the most economical (less time consuming) “programming”. Existing software has been used to check, for example, the validity of the proof of the four color theorem, but the issue here is, at this time and date, what would be best, taking into account the criteria that I mentioned above?

If MO is not the appropriate site for this question, please inform, I am only getting acquainted with what is proper and what is not for this site. I will automatically delete this question if downvotes arrive ...

  • 1
    $\begingroup$ I don't think anyone has done any serious graph theory in Lean yet. But it would not be hard to do. $\endgroup$ Jun 18, 2019 at 18:17
  • $\begingroup$ @NeilStrickland That would be interesting. There is a very interesting (and powerful, with many structural consequences) conjecture which could possibly be settled with the help of a computer ... it is almost made for it ... but from your remark, I take it no one has done any leg work for making graphs accessible in Lean ... maybe a project worth undertaking ... thanks for your comment. $\endgroup$
    – EGME
    Jun 18, 2019 at 18:22

1 Answer 1


One source for an answer might be Craig Larson and some of his websites.... Check out the Graph Brain project and other links from Craig's webpage.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.