4
$\begingroup$

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 ...

Improve this question
$\endgroup$
2
  • 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$
    – Neil Strickland
    Commented 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
    Commented Jun 18, 2019 at 18:22

1 Answer 1

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .