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
    Commented 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
    Commented 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
    Commented 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 ♦
    Commented 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
    Commented 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
    Commented 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
    Commented Dec 5, 2018 at 21:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .