This is from a note I received from Andrew Appel this morning:
You might be interested in this development, all done in the pure functional programming language inside the Coq theorem prover (and proved correct):
http://www.ams.org/notices/200811/tx081101382p.pdf
My mother still has several boxes of original documents from the proof, she was thinking of depositing them in the archives of the U. of Illinois library.
At 10:11 AM 4/29/2013, Hans Havermann wrote:
For those of you who are wondering what a modern reworking of the 4-color-theorem proof might look like, see Georges Gonthier's 2005 "A computer-checked proof of the Four Colour Theorem" here:
http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf
In particular, it is noted on page 10: "Â the version of the Coq system we used needed three days to check our proof, whereas Robertson et al. only needed a three hours... ten years ago! (Future releases of Coq should cut our time back to a few hours, however.)"