20
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ research.microsoft.com/en-us/downloads/… $\endgroup$
    – darij grinberg
    May 1, 2014 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, 2014 at 23:30

1 Answer 1

Reset to default
14
$\begingroup$

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

Improve this answer
$\endgroup$
6
  • 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, 2014 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, 2014 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, 2014 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, 2014 at 4:32
  • 4
    $\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, 2018 at 21:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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