29 Apr
2013
29 Apr
'13
11:12 a.m.
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.)"