A Brief Look At the Four Color Theorem
In the early 1850‟s, a law student named Francis Guthrie pondered over a map of England and noticed the following; on this particular map, each region could be colored using only four different colors such that each region would be designated a different color than the regions that were adjacent to it. (May, Mitchem, Calude, Brun) After making this observation, he wondered if this concept could be expanded to include all possible maps with any arrangement, and posed the question to his brother, Frederick. Not surprisingly, the observation made its way to DeMorgan, who posed the question to his class and even wrote of the observation to his friend Hamilton. Both men observed that they had not heard of a four-coloring theorem before, but while DeMorgan was interested in how one would go about proving its validity, Hamilton stated outright that “… [He was] not likely to attempt your „quaternion of color‟ very soon.” (May)
It was not until almost 27 years later that a proof of the four-color theorem was attempted. In 1878, Cayley questioned the mathematical community about the state of affairs regarding a proof of the four-color theorem. (May) A year later, Alfred Bray Kempe published a proof of the four-color theorem. Though Kempe‟s proof failed to
hold up to scrutiny, in the ten years after he published the proof, Kempe enjoyed fame, prestige, and was even knighted for his work on the four-color theorem. (Calude) His work also introduced what are now called Kempe‟s chains, a new concept that would later be the basis of the current proof. (Saaty)
Figure 1: A shows a four-sided region R that has four regions (Regions 1 – 4) as its
boundaries. Applying the four colors to the surrounding regions produces a partially
colored graph that would require another color to be used for R in the current
B utilizes Kempe‟s chains to change the color assignment of one of the regions in order
to free up a color (in this case, color b) to be used in R without violating the four-color
Kempe‟s chains are used by identifying a region that is at least four-sided and
surrounded by at least 4 regions as the center of a ring. The members of the ring surrounding the central region are colored using four colors. When a contradiction is met, as in Figure 1A above, a pair of colors is evaluated. In the example above, the colors d and b are considered. If a chain of alternating colors d and b exist in the graph connecting two regions, then there must be a chain of alternating colors a and c. If no such chain exists of colors b and d, one of the colors is switched to its partner, allowing the central region to be colored in the resulting free color. (Malkevitch)
When Heawood found Kempe‟s proof to be incomplete in 1890, the example with which he displayed Kempe‟s fault was in fact four-colorable. However, when Kempe‟s
proof was applied to the graph Heawood was using to test the theorem, the method of determining the coloring resulted in an improper coloring. Heawood did not state that Kempe‟s original concepts were completely incorrect, but that the application of his concepts on every possible graph provided a counterexample.
Peter G. Tait also wrote a proof in 1880, where he found an equivalent formulation of the four-color theorem in terms of three-edge coloring, which has been used in other mathematical equations and proofs, though his proof of the four-color theorem was found to be incomplete by Peterson in 1891.
In terms of proof complexity, the four-color theorem is not a difficult theorem to understand. The four-color theorem was even used as the basis for a game for children created by Lewis Carrol, where a player draws a map in order to try and force the other player to use as many colors as possible, while the player filling in the map tries to color it using as few colors as possible. The difficulty in finding a correct proof for the four-color theorem is not in the comprehension of the problem, but in determining a mathematical proof that holds true for any size map with every possible arrangement of its members.
As time progressed, many mathematicians provided proofs for the four-color theorem using limited sets of regions, but no proof was found that would hold true for a complete set of an infinite number of regions. In 1976, Mayer released a proof that was able to hold the four-color theorem true for a set size of 90 regions. As the four-color problem remained unsolved through time, the original conceptual basis for the theorem evolved. The first book on graph theory was published in 1936, and the inclusion of graph theory helped to generalize the four-color conjecture. Instead of looking at the question from a physical map and region-arrangement problem, the four-color theorem was rewritten in terms of planar graph theory. A region therefore became a vertex, and a boundary became an edge that connected two vertices. The theorem was generalized to the following: “In any plane graph each vertex can be assigned exactly one of four colors
so that adjacent vertices have different colors.” A planar graph is defined as a graph drawn in a plane without any of its edges intersecting at a point other than a vertex.
Figure 2. Both A and B are considered planar. Graph B is simple another representation of graph A, but graph B has been drawn to remove the intersecting edges. (Brun)
It was not until 1976 that Appel and Haken released a proof of the four-color theorem that has not yet been disproved, but has acted as the catalyst for an ongoing debate over the nature of proofs. Appel and Haken‟s proof contained over 1200 hours of computational power and used an exhaustive validation of over 1400 examples in order to prove the theorem, using a computational check on each example to determine that it could be four-colored following the original rules of the conjecture.
Appel and Haken, using concepts of reducibility and discharging, created an unavoidable set of configurations, or arrangements of vertices, that would have to be shown to be four-colorable. This unavoidable set is created in such a way that every possible configuration of vertices in a planar graph contained one of the members of this set. In their proof, Appel and Haken were able to show that if a configuration could be reduced to a sub graph that was four-colorable, the whole graph could be four colorable. Discharging is used to find regions of the configuration that could be four colorable. Each vertex in the configuration is given a charge based on its connectivity to other members of the configuration, and all charges add up to 12. By moving charges along the vertices to try to remove the positive and negative charges, the vertices that remain
positively charged are good candidates for a region that could be reducible. Using these tools, Appel and Haken created a computer program containing thousands of lines of code to validate the four-color theorem. Their ultimate goal was to prove the theorem by removing the possibility of a counterexample.
In 1996, a group of mathematicians formulated their own computer-based proof that reduced the unavoidable set size to 633 configurations. (Robertson et al) The proof utilized the work of Appel and Haken, but updated the algorithm used to determine reducibility and discharging, thereby simplifying the set of configurations that needed to be manually checked for the validity in four-coloring. Their rules for discharging especially aiding in the reduction in set size.
Figure 3. A selection of rules for discharging the vertices in the configurations of the unavoidable set. The arrows imply the directionality of the charge-passing. (Robertson et al)
The proof by Appel and Haken, though considered to be valid, has raised debate over computer-based proofs in general. The definition of a proof is “a sequence of statements, each of which is validly derived from those preceding it or is an axiom or assumption, and the final member of which, the conclusion, is the statement of which the truth is thereby established.” (Borowski) Since the Appel and Haken and subsequent proofs are not in the traditional format of a proof, and also rely upon large amounts of behind-the-scenes computation, many members of the mathematical field are still waiting for a proof of the four-color theorem that is in the traditional proof format. Questions also arise regarding the computational aspect of these proofs. The data sets are so large
that a manual check of the configurations would be virtually impossible, which causes many mathematicians to question whether they can trust the results that were produced by the computer‟s calculations. Also, since this theorem was unanswered for so long, many people, mathematicians and otherwise, expect that the proof to this theorem would provide insights or new ideas in mathematics. An exhaustive check on hundreds of configurations does not, on the surface, appear to contribute to the mathematical community. Though the mathematical community does not completely disregard computer-based proofs, many interested parties hope that one day a traditional proof of the four-color theorem, and other theorems, will be found.
Bernhart (1991) Review of Every Planar Map is Four Colorable by Appel and
Haken, American Mathematical Society, Providence RI, 1989
Borowski, EJ, Borwein, JM, The Harper Collins Dictionary of Mathematics, Harper Perennial, 1991
Brun, Yuriy (2002) The Four Color Theorem, MIT Undergraduate Journal of
Mathematics, Cambridge, MA, pp 21-28
Calude, Andreea (2001) The Journey of the Four Colour Theorem Through Time,
The New Zealand Mathematics Magazine, 38:3:27-35
Cayley (1879) On the colouring of maps, Proceedings of the Royal Geographical Society and Monthly Record of Geography New Monthly Series, 1:4:259-261
Malkevitch, Joseph, (2003) Colorful Mathematics: Part I, American Mathematical
Society Feature Column.
May, Kenneth (1965) The Origin of the Four-Color Conjecture, Isis, 56:3:346-
Mitchem, John (1981) On the History and Solution of the Four-Color Map Problem, The Two-Year College Mathematics Journal, 12:2:108-116
Robertson et al (1996) A New Proof of the Four-Colour Theorem, Electronic
Research Announcements of the AMS, 2:1:17-25
Saaty, Thomas (1967) Remarks on the Four Color Problem: the Kempe Catastrophe, Mathematics Magazine, 40:1:31-36
Thomas, Robin (1998) An Update on the Four-Color Theorem, Notices of the
AMS, 45: 7:848-859