Four color theorem (mathematics)

The four-color theorem is a mathematical proposition that holds that any two-dimensional map can be shaded using only four colors in such a way that no two adjoining sections will have the same color. The theorem was first proposed in 1852 and gained widespread attention for more than a century as several mathematicians tried and failed to find a solution. Proof of the theorem was finally obtained in 1976, though many researchers refused to accept its validity as it was obtained using computer-assisted analysis. Subsequent examination of the solution, however, has offered definitive proof of the theorem.

Background

In 1852, mathematician Francis Guthrie, then a law student at University College of London, was coloring in a map of the counties of England when he noticed that he used only four colors to complete the task. He began to theorize that all maps consisting of two-dimensional shapes, or planes, could be completed in the same way using only four colors. Guthrie's theorem held that the countries or geographical shapes could be colored with the four colors so that their borders did not touch a neighboring shape of the same color. The four-color solution did not apply to maps in three dimensions.

While simple maps could be shaded using three or fewer colors, Guthrie proposed that three colors were insufficient for more complicated maps, yet it was not necessary to use five colors. For his purposes, borders were considered lined segments, not the points or corners where the lined boundaries met. In a map of the United States, for example, the states Utah, Colorado, New Mexico, and Arizona meet at a single point. The states diagonal from one another, such as Utah and Arizona or Colorado and New Mexico, may be the same color.

Guthrie mentioned his theory to his younger brother, Frederick, who was also a student at University College. With his brother's permission, Frederick Guthrie submitted the idea to his professor, Augustus De Morgan, a noted mathematician of the era. De Morgan became fixated with the four-color problem, as it came to be called, but struggled to find a solution. He passed the idea on to his colleagues and sought their advice to prove or disprove the theory's validity. While the problem gained some notice in academic circles, it was not seriously studied until the late 1870s, when British mathematician Arthur Cayley outlined the difficulty in solving the theorem and suggested a different approach to the dilemma.

Overview

The problem appeared to be solved in 1879, when British mathematician Alfred Kempe submitted a solution using mathematical "chains" of two colors to predict the patterns of the remaining colors. While Kempe's solution was accepted by the mathematics community, Scottish mathematician Peter Tait disputed the result and proposed his own proof a year later. Kempe's solution was considered valid for about a decade until 1890, when British mathematician Percy John Heawood proved Kempe wrong. Heawood uncovered an error in the color-chain theory that undermined the original solution. Instead, he proposed a five-color theorem suggesting that maps can be colored with no more than five colors. In 1891, Tait's solution was also proven incorrect.

Throughout the twentieth century, mathematicians took on the challenge of the four-color theorem with limited success. Mathematicians easily proved that maps could contain at most six colors, and Heawood's five-color theorem also proved simple to solve, but the four-color problem was more elusive. Much of the work focused on the concept of unavoidable sets, a set of configurations with specific properties that must be contained by at least one member of the set. In 1922, it was proven that a map with at most twenty-five sections could be colored with only four colors. Four years later, proof was found for twenty-eight sections. With each successive solution, the number of sections grew—thirty-two by 1938, thirty-six in 1940, forty in 1970, and ninety by 1976.

That same year, Kenneth Appel and Wolfgang Haken, two mathematicians at the University of Illinois, used a computer to examine multiple examples of maps to find a limit of 1,936 unavoidable configurations that must be present in at least one two-dimensional map. Relying on more than 1,200 hours of computing time, the researchers tested hundreds of thousands of variations of the four-color theorem against the configurations and found the idea to be valid. Despite the lack of flaws in its results, the apparent solution did not appease many mathematicians who thought the use of a computer amounted to nothing more than fact checking and did not offer a reliable verification.

In 1997, a group of mathematicians improved on the work of Appel and Haken. They determined that two-dimensional maps could be reduced to about six hundred basic configurations. They also determined that the four-color theorem could be applied to each of the configurations. While their solution gained more widespread acceptance, it too was arrived at using computer calculations to check each individual case. Some mathematicians wanted a more formal proof of the theorem that did not rely on computers and was not left open to the possibility of programmer error.

In 2004, Georges Gonthier, a mathematician working at the Microsoft Research Laboratory in Cambridge, England, used a computer program called Coq to test the validity of the 1997 solution. Coq was a logic program designed not only to examine the mathematical information used to prove the four-color theorem but also trace the validity of each step of the proofing process. Gonthier and his colleagues determined the 1997 solution—and by association, Appel and Haken's work—was arrived at correctly and definitively proved the four-color theorem.

Bibliography

Calude, Andreea S. "The Journey of the Four Colour Theorem through Time." University of Auckland, Dec. 2000, www.calude.net/andreea/4CT.pdf. Accessed 26 May 2017.

"The Four Color Theorem." Department of Mathematics, University of Illinois, 12 Dec. 2011, www.math.illinois.edu/~lfolwa2/Four%20Color%20Theorem%20Paper.pdf. Accessed 26 May 2017.

"Four-Color Theorem." Wolfram MathWorld, mathworld.wolfram.com/Four-ColorTheorem.html. Accessed 26 May 2017.

Fritsch, Rudolf, and Gerda Fritsch. The Four-Color Theorem: History, Topological Foundations, and Idea of Proof. Translated by Julie Peschke, Springer, 2013.

Gonthier, Georges. "Formal Proof—The Four Color Theorem." American Mathematical Society, Dec. 2008, www.ams.org/notices/200811/tx081101382p.pdf. Accessed 26 May 2017.

O'Connor, J. J., and E. F. Robertson. "The Four Colour Theorem." School of Mathematics and Statistics University of St. Andrews, Sept. 1996, www-history.mcs.st-and.ac.uk/HistTopics/The‗four‗colour‗theorem.html. Accessed 26 May 2017.

Rogers, Leo. "The Four Colour Theorem." University of Cambridge, February 2011, nrich.maths.org/6291. Accessed 26 May 2017.

Wilson, Robin J. Four Colors Suffice: How the Map Problem Was Solved. Princeton UP, 2002.