The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

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