In a 2008 article in the Notices, Georges Gonthier announced a computer-checked proof of the four color theorem using Coq:
Gonthier, Georges. Formal proof—the four-color theorem.
Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. PDF
Unfortunately, the article does not seem to provide a link to the Coq code. Where can I find the code? I'm not having any luck with Google.
Best Answer
It is available on Microsoft's site: http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/default.aspx .
Here is a probably temporarily link to a hopefully complete extracted version in .7z format.
The proof depends on the ssreflect library, for which see http://www.msr-inria.fr/projects/mathematical-components-2/ (thankfully as two .tar.gz files).
edit as noted in the comments an updated, complete version can be obtained from https://github.com/math-comp/fourcolor