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.

  • 1
    $\begingroup$ research.microsoft.com/en-us/downloads/… $\endgroup$ – darij grinberg May 1 '14 at 23:24
  • $\begingroup$ @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... $\endgroup$ – Nate Eldredge May 1 '14 at 23:30

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

  • 1
    $\begingroup$ Thanks very much, darij. I will try to build it on Linux, and if I succeed I'll post further details here. $\endgroup$ – Nate Eldredge May 1 '14 at 23:51
  • $\begingroup$ @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. $\endgroup$ – David Roberts May 2 '14 at 1:25
  • 1
    $\begingroup$ @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. :-( $\endgroup$ – Nate Eldredge May 2 '14 at 3:07
  • 2
    $\begingroup$ 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. $\endgroup$ – darij grinberg May 2 '14 at 4:32
  • 1
    $\begingroup$ The Four Color library has been ported to Coq 8.x and is available at github.com/math-comp/fourcolor $\endgroup$ – Anton Trunov Dec 5 '18 at 21:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.