Four color theorem

The four color theorem is a theorem of mathematics. It says that in any plane surface with regions in it (people think of them as maps), the regions can be colored with no more than four colors. Two regions that have a common border must not get the same color. They are called adjacent (next to each other) if they share a segment of the border, not just a point.^[1]

This was the first theorem to be proved by a computer, in a proof by exhaustion. In proof by exhaustion, the conclusion is established by dividing it into cases, and proving each one separately. There may be a lot of cases. For example, the first proof of the four color theorem was a proof by exhaustion with 1,936 cases. This proof was controversial because most of the cases were checked by a computer program, not by hand. The shortest known proof of the four color theorem today still has over 600 cases.

Even though the problem was first presented as a problem to color political maps of countries, mapmakers are not very interested in it. According to an article by the math historian Kenneth May (Wilson 2002, 2), “Maps utilizing only four colors are rare, and those that do usually require only three. Books on cartography and the history of map making do not mention the four-color property.”

Many simpler maps can be colored using three colors. The fourth color is needed for some maps, such as one in which one region is surrounded by an odd number of others, which touch each other in a cycle. One such example is given in the image. The five color theorem states that five colors are enough to color a map. It has a short, elementary proof and was proven in the late 19th century. (Heawood 1890) Proving that four colors are all that is needed turned out to be much more difficult. Many false proofs and false counterexamples have appeared since the first statement of the four color theorem in 1852.

Intuitively, the four color theorem can be stated as 'given any separation of a plane into contiguous regions, called a map, the regions can be colored using at most four colors so that no two regions which are adjacent have the same color'. To be able to correctly solve the problem, it is necessary to clarify some aspects: First, all points that belong to three or more countries must be ignored. Secondly, bizarre maps with regions of finite area and infinite perimeter can require more than four colors.^[2]

For the purpose of the theorem every "country" has to be a simply connected region, or contiguous. In the real world, this is not true: Alaska as part of the United States, Nakhchivan as part of Azerbaijan, and Kaliningrad as part of Russia are not contiguous. Because the territory of a particular country must be the same color, four colors may not be enough. For instance, consider a simplified map, such as the one shown on the left: In this map, the two regions labeled A belong to the same country, and must be the same color. This map then requires five colors, since the two A regions together are contiguous with four other regions, each of which is contiguous with all the others. If A had only three regions, six or more colors might be needed. In this way, it is possible to make maps that need an arbitrarily high number of colors. A similar construction also applies if a single color is used for all bodies of water, as is usual on real maps.

An easier to state version 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.^[3] 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 that lead without crossing within each region from the vertex location to each shared boundary point of the region. 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 have the same color, or for short, "every planar graph is four-colorable" (Thomas 1998, p. 849; Wilson 2002).

The first person to name the problem was Francis Guthrie, in 1852. He was a law student in England, at the time. He found that he needed at least four colors to color a map of the counties of England.^[4] Augustus de Morgan first discussed the problem, in a letter he wrote to Rowan Hamliton in August 1852. In the letter, de Morgan asks whether four colors are really enough to color a map, such that countries that are next to each other get different colors.

English mathematician Arthur Cayley presented the problem to the mathematical society in London, in 1878. Within a year, Alfred Kempe found what looked like a proof of the problem. Eleven years later, in 1890, Percy Heawood showed that Alfred's proof was wrong. Peter Guthrie Tait presented another attempt at a proof in 1880. It took eleven years to show that Tait's proof did not work either. In 1891, Julius Petersen could show this. When he falsified Cayley's proof, Kempe also showed a proof for a problem he called Five color theorem. The theorem says that any such map can be colored with no more than five colors. There are two restrictions: First, any country is contiguous, there are no exclaves. The second restriction is that countries need to have a common border; if they only touch in a point, they can be colored with the same color. Even though Kempe's proof was wrong, he used some of the ideas which would later permit a correct proof.

In the 1960s and 1970s, Heinrich Heesch developed a first sketch of a proof by computer. Kenneth Appel and Wolfgang Haken improved this sketch in 1976 (Robertson et al. 1996). They were able to reduce the number of cases that would need to be tested to 1936; a later version was made that relied on testing only 1476 cases. Each case needed to be tested by a computer (Appel & Haken 1977) harv error: multiple targets (2×): CITEREFAppelHaken1977 (help).

In 1996, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas improved the method, and reduced the number of cases to be tested to 663. Again, each case needed to be tested by computer.

In 2005, Georges Gonthier and Benjamin Werner developed a formal proof. This was an improvement, because it allowed to use theorem-proving software, for the first time. The software used is called Coq.

The four color theorem is the first big mathematical problem that was proved with the help of a computer. Because the proof cannot be done by a human, some mathematicians did not recognize it as correct. To verify the proof, it is necessary to rely on a correctly working software and hardware to validate the proof. Because the proof was done by computer, it is also not very elegant.

The four color theorem has been notorious for attracting a large number of false proofs and disproofs in its long history. At first, The New York Times refused to report on the Appel–Haken proof. The newspaper did this as a matter of policy; it feared that the proof would be shown false like the ones before it (Wilson 2002, p. 209). Some proofs took a long time, till they could be falsified: For Kempe's and Tait's proofs falsifying them took over a decade.

The map (left) has been colored with five colors, and it is necessary to change at least four of the ten regions to obtain a coloring with only four colors (right).

The simplest counterexamples generally try to create one region which touches all the others. This forces the remaining regions to be colored with only three colors. Because the four color theorem is true, this is always possible; however, because the person drawing the map is focused on the one large region, they do not notice that the remaining regions can in fact be colored with three colors.

This trick can be generalized: If the colors of some regions in a map are chosen beforehand, it becomes impossible to color the remaining regions in such a way that in total, only four colors are used. Someone verifying the counterexample may not think that it may be needed to change the color of these regions. This will make the counterexample look valid, even though it is not.

Perhaps one effect underlying this common misconception is the fact that the color restriction is not transitive: a region only has to be colored differently from regions it touches directly, not regions touching regions that it touches. If this were the restriction, planar graphs would require arbitrarily large numbers of colors.

Other false disproofs violate the assumptions of the theorem in unexpected ways, such as using a region that has multiple disconnected parts, or not allowing regions of the same color from touching at a point.

In real life, many countries have exclaves or colonies. Since they belong to the country, they need to be colored with the same color as the parent country. This means that usually, more than four colors are needed to color such a map. When mathematicians talk about the graph associated with the problem, they say that is not planar. Even though it is easy to check if a graph is planar, finding the fewest number of colors needed to color it is very difficult. It is NP-complete, which is one of the most difficult problems that exist. The fewest number of colors needed to color a graph is known as its chromatic number. Many of the problems that happen when trying to solve the four color theorem are related to discrete mathematics. For this reason, methods from algebraic topology are often used.

The four color theorem requires the "map" to be on a flat surface, what mathematicians call a plane. In 1890, Percy John Heawood created what is called Heawood conjecture today: It asks the same question as the four color theorem, but for any topological object. As an example, a torus can be colored with at most seven colors. The Heawood conjecture gives a formula that works for all such objects, except the Klein bottle.

• Allaire, F. (1997), "Another proof of the four colour theorem—Part I", Proceedings, 7th Manitoba Conference on Numerical Mathematics and Computing, Congr. Numer., vol. 20, pp. 3–72
• Appel, Kenneth; Haken, Wolfgang (1977), "Every Planar Map is Four Colorable Part I. Discharging", Illinois Journal of Mathematics, vol. 21, pp. 429–490
• Appel, Kenneth; Haken, Wolfgang; Koch, John (1977), "Every Planar Map is Four Colorable Part II. Reducibility", Illinois Journal of Mathematics, vol. 21, pp. 491–567
• Appel, Kenneth; Haken, Wolfgang (October 1977), "Solution of the Four Color Map Problem", Scientific American, vol. 237, no. 4, pp. 108–121, Bibcode:1977SciAm.237d.108A, doi:10.1038/scientificamerican1077-108
• Appel, Kenneth; Haken, Wolfgang (1989), Every Planar Map is Four-Colorable (PDF), Providence, RI: American Mathematical Society, ISBN 0-8218-5103-9
• Bernhart, Frank R. (1977), "A digest of the four color theorem", Journal of Graph Theory, vol. 1, no. 3, pp. 207–225, doi:10.1002/jgt.3190010305
• Borodin, O. V. (1984), "Solution of the Ringel problem on vertex-face coloring of planar graphs and coloring of 1-planar graphs", Metody Diskretnogo Analiza (41): 12–26, 108, MR 0832128.
• Cayley, Arthur (1879), "On the colourings of maps", Proc. Royal Geographical Society, vol. 1, no. 4, Blackwell Publishing, pp. 259–261, doi:10.2307/1799998, JSTOR 1799998

• Fritsch, Rudolf; Fritsch, Gerda (1998), The Four Color Theorem: History, Topological Foundations and Idea of Proof, New York: Springer, ISBN 978-0-387-98497-1
• Gonthier, Georges (2008), "Formal Proof—The Four-Color Theorem" (PDF), Notices of the American Mathematical Society, vol. 55, no. 11, pp. 1382–1393
• Gonthier, Georges (2005), A computer-checked proof of the four colour theorem (PDF), unpublished
• Hadwiger, Hugo (1943), "Über eine Klassifikation der Streckenkomplexe", Vierteljschr. Naturforsch. Ges. Zürich, 88: 133–143
• Heawood, P. J. (1890), "Map-Colour Theorem", Quarterly Journal of Mathematics, Oxford, vol. 24, pp. 332–338
• Magnant, C.; Martin, D. M. (2011). "Coloring rectangular blocks in 3-space". Discussiones Mathematicae Graph Theory. 31 (1): 161–170. doi:10.7151/dmgt.1535.
• Nash-Williams, C. St. J. A. (1967), "Infinite graphs—a survey", J. Combinatorial Theory, 3 (3): 286–301, doi:10.1016/S0021-9800(67)80077-2, MR 0214501.
• O'Connor; Robertson (1996), The Four Colour Theorem, MacTutor archive, archived from the original on 2013-01-16, retrieved 2013-02-22
• Pegg, Ed, Jr.; Melendez, J.; Berenguer, R.; Sendra, J. R.; Hernandez, A.; Del Pino, J. (2002), "Book Review: The Colossal Book of Mathematics" (PDF), Notices of the American Mathematical Society, 49 (9): 1084–1086, Bibcode:2002ITED...49.1084A, doi:10.1109/TED.2002.1003756{{citation}}: CS1 maint: multiple names: authors list (link)
• Reed, Bruce; Allwright, David (2008), "Painting the office", Mathematics-in-Industry Case Studies, 1: 1–8, archived from the original on February 3, 2013, retrieved February 22, 2013
• Ringel, G.; Youngs, J.W.T. (1968), "Solution of the Heawood Map-Coloring Problem", Proc. Nat. Acad. Sci. USA, vol. 60, no. 2, pp. 438–445, Bibcode:1968PNAS...60..438R, doi:10.1073/pnas.60.2.438, PMC 225066, PMID 16591648
• Robertson, Neil; Sanders, Daniel P.; Seymour, Paul; Thomas, Robin (1996), "Efficiently four-coloring planar graphs", Proceedings of the twenty-eighth annual ACM symposium on Theory of computing - STOC '96, STOC'96: Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, ACM Press, pp. 571–575, doi:10.1145/237814.238005, ISBN 0897917855, S2CID 14962541
• Robertson, Neil; Sanders, Daniel P.; Seymour, Paul; Thomas, Robin (1997), "The Four-Colour Theorem", J. Combin. Theory Ser. B, vol. 70, no. 1, pp. 2–44, doi:10.1006/jctb.1997.1750
• Saaty, Thomas; Kainen, Paul (1986), "The Four Color Problem: Assaults and Conquest", Science, 202 (4366), New York: Dover Publications: 424, Bibcode:1978Sci...202..424S, doi:10.1126/science.202.4366.424, ISBN 0-486-65092-8, PMID 17836752
• Swart, ER (1980), "The philosophical implications of the four-color problem" (PDF), American Mathematical Monthly, vol. 87, no. 9, Mathematical Association of America, pp. 697–702, doi:10.2307/2321855, JSTOR 2321855, archived from the original (PDF) on July 14, 2010, retrieved February 22, 2013
• Thomas, Robin (1998), "An Update on the Four-Color Theorem" (PDF), Notices of the American Mathematical Society, vol. 45, no. 7, pp. 848–859
• Thomas, Robin (1995), The Four Color Theorem, archived from the original on 2020-02-14, retrieved 2013-02-22
• Thomas, Robin, Recent Excluded Minor Theorems for Graphs (PDF), p. 14, archived from the original (PDF) on 2016-08-03, retrieved 2013-02-22
• Wilson, Robin (2002), Four Colors Suffice, London: Penguin Books, ISBN 0-691-11533-8

• Chechulin V. L. About а one proof of a planar's graphs 4-chromatically http://www.uresearch.psu.ru/files/articles/17_89592.doc^{[permanent dead link]}

• WikiBooks:Famous Theorems of Mathematics/Four color theorem