“Richard Zach reports”:http://www.ucalgary.ca/~rzach/logblog/2005/04/four-color-theorem-verified-in-coq.html that Georges Gonthier has a paper verifying the four colour map theorem. I found this odd, since I thought that “Hud Hudson”:http://www.ac.wwu.edu/%7Earistos/BooksPapers.html had shown that the theorem is not actually true, at least not as typically stated. Hudson’s proof is “here”:http://proquest.umi.com/pqdweb?index=18&did=358630871&SrchMode=3&sid=1&Fmt=4&VInst=PROD&VType=PQD&RQT=309&VName=PQD&TS=1114107341&clientId=8424&aid=1 though that link may not be accessible to everyone.