The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

For the record, the old sources can be found at
  http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

The Coq version required is listed (8.0pl2+), but the ssreflect version used may not be available anymore (the ssreflect releases on the Mathematical Components webpage are for Coq 8.4). It will still be useful if you want to read the proof.

If you are interested in this proof, you should definitely read Georges Gonthier's accompanying article, "A computer-checked proof of the Four Colour Theorem",
  http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf
The first 16 pages of this 57-pages document give a readable outline of the proof (which is not purely a Coq formalization of existing proof, but in many details entirely new) and the formalization approach. The rest is a detailed explanation of the complete proof argument.

On Sun, Aug 10, 2014 at 8:44 AM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Sat, Aug 09, 2014 at 10:37:53AM +0800, coqcdp wrote:
> Dear friends,
>                      Currently , I heard about that someone has proved "the four colour theorem" with coq. Really? Can I run it in my PC?
>             Where can I get the source code ? And is there anyone who has ever run it successfully in PC?

You are right, the 4ct has been completely formalized in Coq.
The source code has been hard to publish for licensing issues (that are
now solved but a new public release did not happen yet).
If you google for Georges Gonthier and 4ct you will probably find the old
release, but it runs on old Coq versions.
If you are interested you can probably get access to the svn repository
in which the up to date code actually lives by asking on the ssreflect
mailing list.
http://www.msr-inria.fr/projects/mathematical-components-2/
(link in the downloads tab)

Best

>
>       Yours sincerely ,
>                                  D.P.Chen.

--
Enrico Tassi