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:
http://people.math.gatech.edu/~thomas/FC/fourcolor.html
Please note that Georgia Tech is redesigning its web pages and this link might become ineffective some time soon.
