most recent 30 from http://mathoverflow.net 2013-05-25T23:07:00Z http://mathoverflow.net/feeds/question/41121 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/41121/four-color-proof garfield 2010-10-05T09:36:17Z 2010-10-06T02:04:20Z

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

http://mathoverflow.net/questions/41121/four-color-proof/41124#41124 Ben 2010-10-05T10:44:07Z 2010-10-05T10:44:07Z

<p>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.</p> <p>For a paper, see Gonthier, Georges (2008), "<a href="http://www.ams.org/notices/200811/tx081101382p.pdf" rel="nofollow">Formal Proof--The Four-Color Theorem</a>", Notices of the American Mathematical Society 55 (11): 1382–1393</p>

http://mathoverflow.net/questions/41121/four-color-proof/41164#41164 Joseph O'Rourke 2010-10-05T15:00:46Z 2010-10-05T15:00:46Z

<p>Just as background, definitely not an answer to your question: You are probably aware of the paper, "<a href="http://www.ams.org/journals/era/1996-02-01/S1079-6762-96-00003-0/home.html" rel="nofollow">A new proof of the four colour theorem</a>," by N. Robertson, D. P. Sanders, P. D. Seymour and R. Thomas, in <em>Electron. Res. Announc. Amer. Math. Soc.</em> 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."</p>

http://mathoverflow.net/questions/41121/four-color-proof/41166#41166 Gerald Edgar 2010-10-05T15:05:40Z 2010-10-06T02:04:20Z

<p>from review <a href="http://www.ams.org/mathscinet-getitem?mr=1403921" rel="nofollow">http://www.ams.org/mathscinet-getitem?mr=1403921</a> of a survey paper by Paul Seymour, we find...</p> <blockquote> <p>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. </p> </blockquote>