The four colour theorem
Prove that the regions of any map drawn in the plane can be colored with at most four colors so that any two regions sharing a border of positive length get different colors. Equivalently, prove that every planar graph is 4-colorable.
History and references
Solved in 1976 by Kenneth Appel and Wolfgang Haken.
Francis Guthrie noticed in 1852, while coloring a map of the counties of England, that four colors seemed to suffice, and the question spread through Augustus De Morgan. Five colors are easy to prove sufficient, but four resisted many false proofs and counterexamples. In 1976 Kenneth Appel and Wolfgang Haken reduced the problem to a large finite set of configurations and checked them by computer, the first major theorem proved this way. Robertson, Sanders, Seymour and Thomas simplified the argument in 1997 to 633 configurations, and in 2005 Georges Gonthier verified a proof in a general-purpose proof assistant. All known proofs still rely on a computer to check a long list of cases.
References
Solutions 0
Sign in or create an account to publish a solution