Editing Four color theorem (section)

{{short description|Statement in mathematics}}
[[File:Four Colour Map Example.svg|thumb|Example of a four-colored map]][[File:Map of United States accessible colors shown.svg|thumb|A four-colored map of the states of the United States (ignoring lakes and oceans)]]

In [[mathematics]], the '''four color theorem''', or the '''four color map theorem''', states that no more than four colors are required to color the regions of any map so that no two adjacent regions have the same color. ''Adjacent'' means that two regions share a common boundary of non-zero length (i.e., not merely a corner where three or more regions meet).<ref>From {{harvtxt|Gonthier|2008}}: "Definitions: A planar map is a set of pairwise disjoint subsets of the plane, called regions. A simple map is one whose regions are connected open sets. Two regions of a map are adjacent if their respective closures have a common point that is not a corner of the map. A point is a corner of a map if and only if it belongs to the closures of at least three regions. Theorem: The regions of any simple planar map can be colored with only four colors, in such a way that any two adjacent regions have different colors."</ref> It was the first major [[theorem]] to be [[computer-assisted proof#Theorems proved with the help of computer programs|proved using a computer]]. Initially, this [[Mathematical proof|proof]] was not accepted by all mathematicians because the [[computer-assisted proof]] was [[Non-surveyable proof|infeasible for a human to check by hand]].{{sfnp|Swart|1980}} The proof has gained wide acceptance since then, although some doubts remain.{{sfnp|Wilson|2014|loc=216–222}}

The theorem is a stronger version of the [[five color theorem]], which can be shown using a significantly simpler argument. Although the weaker five color theorem was proven already in the 1800s, the four color theorem resisted until 1976 when it was proven by [[Kenneth Appel]] and [[Wolfgang Haken]] in a [[Computer-assisted proof|computer-aided proof]]. This came after many false proofs and mistaken counterexamples in the preceding decades.

The Appel–Haken proof proceeds by analyzing a very large number of reducible configurations. This was improved upon in 1997 by Robertson, Sanders, Seymour, and Thomas, who have managed to decrease the number of such configurations to 633 – still an extremely long case analysis. In 2005, the theorem was verified by [[Georges Gonthier]] using a general-purpose [[proof assistant|theorem-proving software]].