# Where can I find Gonthier's Coq code proving the four color theorem?

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.

-
@darijgrinberg: Thanks, maybe that should be posted as an answer. It's annoying that it's in a proprietary Microsoft packaging format, but given that Gonthier works for Microsoft I guess maybe I shouldn't be surprised... –  Nate Eldredge May 1 '14 at 23:30

## 1 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).

-
Thanks very much, darij. I will try to build it on Linux, and if I succeed I'll post further details here. –  Nate Eldredge May 1 '14 at 23:51
@NateEldredge - I wonder what the license is on the code. Ideally it could be stored in an online version control repository of some kind, so that people could make use of it. –  David Roberts May 2 '14 at 1:25
@DavidRoberts: Each file says at the top (c) Copyright Microsoft Corporation and Inria. All rights reserved. I didn't see any further license information. But that makes it look like it's probably not allowed. :-( –  Nate Eldredge May 2 '14 at 3:07
@NateEldredge - hmph. :-( indeed. –  David Roberts May 2 '14 at 3:14
You should ask Gonthier -- he and his team seem to usually release with the CeCILL licenses, so this might just be a minor technicality they didn't bother to clarify. –  darij grinberg May 2 '14 at 4:32