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.