## four color proof [closed]

Has four color proof been proved without the help of computer?Where can I find the paper?

-
There's a huge amount to say about 4CC and its various proofs, which probably people will say below in the answers. But the short answer to your first question is "no". – Kevin Buzzard Oct 5 2010 at 9:41
(i) Not as far as I am aware. (ii) What paper? – Robin Chapman Oct 5 2010 at 9:42

## closed as not a real question by Robin Chapman, gowers, Daniel Moskovich, Pete L. Clark, Andrea FerrettiOct 6 2010 at 8:55

No, but the proof has been formalized into computer-checkable form, using the proof-assistant Coq. As far as I know, the proof still relies on enumeration of cases and is therefore quite tedious.

For a paper, see Gonthier, Georges (2008), "Formal Proof--The Four-Color Theorem", Notices of the American Mathematical Society 55 (11): 1382–1393

-
I've heard from my colleague Wilbert van der Kallen that the formal proof of the four colour theorem was written over a time interval that was so long, that various parts of he proof have been made to compile over various versions of Coq. The problem is that these versions of Coq are not backwards compatible! So, formally speaking there is no single computed verified proof of the four colour theorem. What there is is a collection of computed checked pieces that, together, assemble into a proof. – André Henriques Oct 5 2010 at 12:46
Why are there various versions of Coq? Presumably because the early versions contain bugs, which then invalidate the certificates for the earlier parts of the proof ;-) – Kevin Buzzard Oct 5 2010 at 14:59
And by pessimistic meta-induction (i.e. the fact that there may well be future versions of Coq) doesn't this mean that we shouldn't believe the parts verified with the current version? ;-) – Kevin Buzzard Oct 5 2010 at 15:01
Different versions of Coq differ in the libraries of theories and tactics and other, often superficial, features. The core logic remains the same. – supercooldave Oct 5 2010 at 15:15
@Kevin: By design, one need worry only if changes were made to the (small, stable) type-checking kernel. The other machinery (which may be incompatible in various versions) can be seen as an evolving set of tools for making the construction of kernel-checkable proofs easier. – Grant Olney Passmore Oct 5 2010 at 15:41
 Replace the .proxy.lib.ohio-state.edu with the EZProxy syntax of your institution, as appropriate. :) – J. M. Oct 5 2010 at 15:13 See my parallel posting linking to that paper. This is from the [RSST] Abstract: "Here we announce another proof, still using a computer, but simpler than Appel and Haken's in several respects." – Joseph O'Rourke Oct 5 2010 at 15:31 I edited out the proxy portion of the URL. – David Speyer Oct 6 2010 at 2:04