Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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.

share|improve this question
1  
    
@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 at 23:30

1 Answer 1

up vote 4 down vote accepted

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

share|improve this answer
1  
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 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 at 1:25
1  
@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 at 3:07
    
@NateEldredge - hmph. :-( indeed. –  David Roberts May 2 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 at 4:32

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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