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](http://www.ams.org/notices/200811/tx081101382p.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.



Where can I find Gonthier's Coq code proving the four color theorem?
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](http://www72.zippyshare.com/v/28567991/file.html) 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> 


