The four color theorem is a theorem about graphs (as in graphs and networks) and it was proved with the aid of a computer. To date, there is no hand-checkable proof. The software that was used to verify the four color theorem is publicly available and hosted at the website of one of the authors of the only proof (that I am aware of) that is certifiably correct. The authors of the proof are Robertson, Sanders, Seymour, and Thomas. The correctness checking was done by Gonthiers. I am wondering whether there is an implementation in Mathematica of the software used by Robertson et al. in their proof, and in general, of software that would be useful for the kinds of questions these authors dealt with.

A good place to start if you are interested in this is:


Please note that Georgia Tech is redesigning its web pages and this link might become ineffective some time soon.

  • 1
    $\begingroup$ Welcome to Mathematica Stack Exchange. Please make the question self-contained as most people here may not know about the proof you are referring to. $\endgroup$
    – C. E.
    May 18 '19 at 19:16
  • $\begingroup$ Thank you, I have edited the question. $\endgroup$
    – EGME
    May 18 '19 at 19:29
  • $\begingroup$ Maybe you could add some DOI links to the relevant papers and Wikipedia articles? Otherwise everybody has to look them up again. $\endgroup$
    – Roman
    May 18 '19 at 19:33
  • 1
    $\begingroup$ I have added the best link I could think of. That link has links to the mathematical papers and the software repository, although take note that the university where this is hosted is redesigning its web pages, so some of the links in this page which I accessed 2019.may.18 at 22.42 might already be broken ... this one is still there. $\endgroup$
    – EGME
    May 18 '19 at 19:46
  • 1
    $\begingroup$ Removed the igraphm tag. IGraph/M has functionality to compute minimum vertex colourings, but not to prove the four colour theorem. $\endgroup$
    – Szabolcs
    May 18 '19 at 20:16