# four color proof [closed]

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

-

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

It's difficult to tell what is being asked here. This question is ambiguous, vague, incomplete, overly broad, or rhetorical and cannot be reasonably answered in its current form. For help clarifying this question so that it can be reopened, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

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 '10 at 9:41
(i) Not as far as I am aware. (ii) What paper? – Robin Chapman Oct 5 '10 at 9:42

## 3 Answers

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 '10 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 '10 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 '10 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 '10 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 '10 at 15:41

Just as background, definitely not an answer to your question: You are probably aware of the paper, "A new proof of the four colour theorem," by N. Robertson, D. P. Sanders, P. D. Seymour and R. Thomas, in Electron. Res. Announc. Amer. Math. Soc. 2 (1996), 17-25 (electronic). It is still a computer proof, but simpler than Appel and Haken's: "Our unavoidable set has size 633 as opposed to the 1476 member set of Appel and Haken, and our discharging method uses only 32 discharging rules, instead of the 300+ of Appel and Haken."

-

from review http://www.ams.org/mathscinet-getitem?mr=1403921 of a survey paper by Paul Seymour, we find...

In 1993, Seymour, Neil Robertson, Daniel Sanders, and Robin Thomas, after trying to read the Appel-Haken proof, decided to supply their own proof, in which the data are available in electronic form, which can be checked by hand or computer. They confirmed that the four-color theorem is true and provable by the approach used by Appel and Haken.

-
Replace the .proxy.lib.ohio-state.edu with the EZProxy syntax of your institution, as appropriate. :) – J. M. Oct 5 '10 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 '10 at 15:31
I edited out the proxy portion of the URL. – David Speyer Oct 6 '10 at 2:04