Problem 2.1: Four-Color Theorem

N. Robertson, D.P. Sanders, P. Seymour, and R. Thomas "The Four-Colour Theorem", Manuscript.

Abstract: "The four-colour theorem, that every loopless planar graph admits a vertex-colouring with at most four different colours, was proved in 1976 by Appel and Haken, using a computer. Here we give another proof, still using a computer, but simpler in several respects than Appel and Haken's."

( A copy of the manuscript is available from the authors. Computer files supporting the proof can be obtained via anonymous ftp - login as "anonymous" and give your e-mail address as password - from ftp.math.gatech.edu located in the directory pub/users/thomas/four )

An interesting and very well presented summary of the new proof can be found on the WWW under the address:
http://www.math.gatech.edu/~thomas/FC/fourcolor.html

A history of the four-color theorem can be found on the WWW under the address: http://www-groups.dcs.st-and.ac.uk:80/~history/HistTopics/The_four_colour_theorem.html

December, 1994 Bjarne Toft

The problem of deciding 3-colourability of a 4-regular graph mentioned on pages 34-35 was proved NP-complete already in 1980 in the paper:

D.P. Dailey, Uniqueness of colorability and colorability of planar 4-regular graphs are NP-complete, Discrete Math. 30 (1980), 289-293.

Hence our suggestion of a possible approach to McGuinness' question is not feasible!
The existence of 2-connected 4-regular planar graphs that are 4-chromatic also follows constructively from Dayley's paper.
We are grateful to Stefan Hougardy for informing us about the paper by Dailey (by e-mail in August 1996).

November, 1996 Bjarne Toft

The new proof of the four-color theorem mentioned in the above December 1994 note has appeared:

N. Robertson, D. Sanders, P. Seymour, and R. Thomas, The Four-Colour Theorem, J. Combin. Theory Ser. B 70 (1997), 2-44.

August, 1997 Bjarne Toft

The paper

G. Gonthier, Formal Proof - The Four-Color Theorem, Notices Amer. Math. Soc. 55 (2008), 1382-1393

explains a proof of the four-color theorem which can be checked by a formal proof checking procedure. Thus the checking is still performed by a computer, but using software capable of checking general mathematical proofs, and not tailored to the four-color problem specifically.

September, 2010 Tommy R. Jensen

The following article describes a proof of the four-color theorem which uses exclusively D-reducible configurations.

J.P. Steinberger, An unavoidable set of D-reducible configurations, Trans. Amer. Math. Soc. 362 (2010) 6633-6661.

September, 2010 Tommy R. Jensen

Back to Overview menu
Back to Graph Coloring Problems homepage

Last modified August 5, 1997 Bjarne Toft