The coloring of maps can also be stated in terms of
graph theory, by considering it in terms of constructing a
graph coloring of the
planar graph of adjacencies between regions. In graph-theoretic terms, the theorem states that for a
loopless planar graph G, denoting by \chi(G) its
chromatic number, \chi(G) \leq 4. For this to be meaningful, the intuitive statement of the four color theorem – "given any separation of a plane into contiguous regions, the regions can be colored using at most four colors so that no two adjacent regions have the same color" – needs to be interpreted appropriately. First, regions are adjacent if they share a boundary segment; two regions that share only isolated boundary points are not considered adjacent. (Otherwise, a map in a shape of a
pie chart would make an arbitrarily large number of regions 'adjacent' to each other at a common corner, and require an arbitrarily large number of colors as a result.) Second, bizarre regions, such as those with finite area but infinitely long perimeter, are not allowed; maps with such regions can require more than four colors. (To be safe, we can restrict to regions whose boundaries consist of finitely many straight line segments. It is allowed that a region has
enclaves, that is it entirely surrounds one or more other regions.) Note that the notion of "contiguous region" (technically:
connected open subset of the plane) is not the same as that of "country" on regular maps, since a country need not be contiguous: it may have
exclaves, like
Angola with its
Cabinda Province,
Azerbaijan with its
Nakhchivan Autonomous Republic, Russia with its
Kaliningrad Oblast,
France with its
overseas territories, and the
United States with the state of
Alaska. If we require the entire territory of a country to receive the same color, then four colors are not always sufficient. For instance, consider the simplified map: In this map, the two regions labeled
A belong to the same country. If we want those regions to receive the same color, then five colors are required, since the two
A regions together are adjacent to four other regions, each of which is adjacent to every other. A simpler statement of the theorem uses
graph theory. The set of regions of a map can be represented more abstractly as an
undirected graph that has a
vertex for each region and an
edge for every pair of regions that share a boundary segment. This graph is
planar: it can be drawn in the plane without crossings by placing each vertex at an arbitrarily chosen location within the region to which it corresponds, and by drawing the edges as curves without crossings that lead from one region's vertex, across a shared boundary segment, to an adjacent region's vertex. Conversely, any planar graph can be formed from a map in this way. In graph-theoretic terminology, the four-color theorem states that the vertices of every planar graph can be colored with at most four colors so that no two adjacent vertices receive the same color, or for short: every planar graph is
four-colorable. ==History==
Early proof attempts , 23 Oct. 1852 As far as is known, the conjecture was first proposed on October 23, 1852, when
Francis Guthrie, while trying to color the map of counties of England, noticed that only four different colors were needed. At the time, Guthrie's brother,
Frederick, was a student of
Augustus De Morgan (the former advisor of Francis) at
University College London. Francis inquired with Frederick regarding it, who then took it to De Morgan. (Francis Guthrie graduated later in 1852, and later became a professor of mathematics in South Africa.) According to De Morgan: A student of mine [Guthrie] asked me to day to give him a reason for a fact which I did not know was a fact—and do not yet. He says that if a figure be any how divided and the compartments differently colored so that figures with any portion of common boundary
line are differently colored—four colors may be wanted but not more—the following is his case in which four colors
are wanted. Query cannot a necessity for five or more be invented... "F.G.", perhaps one of the two Guthries, published the question in
The Athenaeum in 1854, and De Morgan posed the question again in the same magazine in 1860. Another early published reference by in turn credits the conjecture to De Morgan. There were several early failed attempts at proving the theorem. De Morgan believed that it followed from a simple fact about four regions, though he didn't believe that fact could be derived from more elementary facts. This arises in the following way. We never need four colours in a neighborhood unless there be four counties, each of which has boundary lines in common with each of the other three. Such a thing cannot happen with four areas unless one or more of them be inclosed by the rest; and the colour used for the inclosed county is thus set free to go on with. Now this principle, that four areas cannot each have common boundary with all the other three without inclosure, is not, we fully believe, capable of demonstration upon anything more evident and more elementary; it must stand as a postulate. another was given by
Peter Guthrie Tait in 1880. It was not until 1890 that Kempe's proof was shown incorrect by
Percy Heawood, and in 1891, Tait's proof was shown incorrect by
Julius Petersen—each false proof stood unchallenged for 11 years. In 1890, in addition to exposing the flaw in Kempe's proof, Heawood proved the
five color theorem and generalized the four color conjecture to surfaces of arbitrary
genus. Tait, in 1880, showed that the four color theorem is equivalent to the statement that a certain type of graph (called a
snark in modern terminology) must be non-
planar. In 1943,
Hugo Hadwiger formulated the
Hadwiger conjecture, a far-reaching generalization of the four-color problem that still remains unsolved.
Proof by computer During the 1960s and 1970s, the German mathematician
Heinrich Heesch developed methods of using computers to search for a proof. Notably, he was the first to use
discharging for proving the theorem, which turned out to be important in the unavoidability portion of the subsequent Appel–Haken proof. He also expanded on the concept of reducibility and, along with Ken Durre, developed a computer test for it. Unfortunately, at this critical juncture, he was unable to procure the necessary supercomputer time to continue his work. Others took up his methods, including his computer-assisted approach. While other teams of mathematicians were racing to complete proofs,
Kenneth Appel and
Wolfgang Haken at the
University of Illinois announced, on June 21, 1976, that they had proved the theorem. They were assisted in some algorithmic work by
John A. Koch. If the four-color conjecture were false, there would be at least one map with the smallest possible number of regions that requires five colors. The proof showed that such a minimal counterexample cannot exist, through the use of two technical concepts: • An
unavoidable set is a set of configurations such that every map that satisfies some necessary conditions for being a minimal non-4-colorable
triangulation (such as having minimum degree 5) must have at least one configuration from this set. • A
reducible configuration is an arrangement of countries that cannot occur in a minimal counterexample. If a map contains a reducible configuration, the map can be reduced to a smaller map. This smaller map has the condition that if it can be colored with four colors, this also applies to the original map. This implies that if the original map cannot be colored with four colors the smaller map cannot either and so the original map is not minimal. Using mathematical rules and procedures based on properties of reducible configurations, Appel and Haken found an unavoidable set of reducible configurations, thus proving that a minimal counterexample to the four-color conjecture could not exist. Their proof reduced the infinitude of possible maps to 1,834 reducible configurations (later reduced to 1,482) which had to be checked one by one by computer and took over a thousand hours. This reducibility part of the work was independently double checked with different programs and computers. However, the unavoidability part of the proof was verified in over 400 pages of
microfiche, which had to be checked by hand with the assistance of Haken's daughter
Dorothea Blostein. Appel and Haken's announcement was widely reported by the news media around the world, and the math department at the
University of Illinois used a postmark stating "Four colors suffice." At the same time, the unusual nature of the proof—it was the first major theorem to be proved with extensive computer assistance—and the complexity of the human-verifiable portion aroused considerable controversy. Not all mathematicians accepted that a computer-based demonstration could qualify as a genuine proof. Even some of those who did, like
Ian Stewart, found the proof unsatisfying, since it fell out as a
fait accompli and lacked a sense of structure. "The answer appears as a kind of monstrous coincidence," wrote Stewart.
H. S. M. Coxeter found it "very unlikely that anyone can break that proof down into something that one would regard as an ordinary proof". In the early 1980s, rumors spread of a flaw in the Appel–Haken proof. Ulrich Schmidt at
RWTH Aachen had examined Appel and Haken's proof for his master's thesis that was published in 1981. He had checked about 40% of the unavoidability portion and found a significant error in the discharging procedure . In 1986, Appel and Haken were asked by the editor of
Mathematical Intelligencer to write an article addressing the rumors of flaws in their proof. They replied that the rumors were due to a "misinterpretation of [Schmidt's] results" and obliged with a detailed article. Their
magnum opus,
Every Planar Map is Four-Colorable, a book claiming a complete and detailed proof (with a microfiche supplement of over 400 pages), appeared in 1989; it explained and corrected the error discovered by Schmidt as well as several further errors found by others.
Simplification and verification Since the proving of the theorem, a new approach has led to both a shorter proof and a more efficient algorithm for 4-coloring maps. In 1996,
Neil Robertson,
Daniel P. Sanders,
Paul Seymour, and
Robin Thomas created a
quadratic-time algorithm (requiring only
O(
n2) time, where
n is the number of vertices), improving on a
quartic-time algorithm based on Appel and Haken's proof. The new proof, based on the same ideas, is similar to Appel and Haken's but more efficient because it reduces the complexity of the problem and requires checking only 633 reducible configurations. Both the unavoidability and reducibility parts of this new proof must be executed by a computer and are impractical to check by hand. In 2001, the same authors announced an alternative proof, by proving the
snark conjecture. This proof remains unpublished, however. In 2005,
Benjamin Werner and
Georges Gonthier formalized a proof of the theorem inside the
Coq proof assistant. This removed the need to trust the various computer programs used to verify particular cases; it is only necessary to trust the Coq kernel. ==Summary of proof ideas==