I'm way out of date. The proof (discretized using hypermaps instead of graphs) was completely formalized in Coq in 2005: http://research.microsoft.com/en-us/um

I'm way out of date. The proof (discretized using hypermaps instead of graphs) was completely formalized in Coq in 2005: http://research.microsoft.com/en-us/um/people/gonthier/4colproof.pdf http://research.microsoft.com/en-us/um/people/gonthier/4colp...