2

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

flag
6 
 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
8 
 (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 Ferretti Oct 6 2010 at 8:55

3 Answers

8

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

link|flag
3 
 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
2 
 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
2 
 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
3 
 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
2 
 @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
show 5 more comments
3

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."

link|flag
2

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.

link|flag
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

Not the answer you're looking for? Browse other questions tagged or ask your own question.