Photo Credit: Stephanie Blanda
This weekend, I was helping paint flats for a play when an interesting problem arose – we wanted to use three colors of paint to create rectangles of different sizes on a rectangular flat, with the stipulation that no two adjacent rectangles were the same color. Prior to painting, we labeled the rectangles with their colors just to make sure everything worked out. We didn’t run into any problems, but one person did ask the question – was it possible to come up with a configuration of rectangles that was impossible to paint with our condition? Since we were only using three colors of paint, the answer, of course, was yes! In fact, when making up sample designs the night before, our director ran into the issue of three colors not being enough.
In mathematics, the Four Color Theorem (or Map Coloring Problem) states that, given any separation of a plane into contiguous regions (producing a figure we will call a map), no more than four colors are required to color the regions of the map so that no two adjacent regions have the same color. For this problem, two regions are considered adjacent if they share a boundary that is not just a corner. It seems like a simple problem – given a map, how many colors do you need so that no two adjacent regions are the same color? However, this problem, so simply stated in 1852, was tantalizingly difficult to prove, leading to many false proofs and false counterexamples. It was not until 1976 that, with the aid of a computer, a proof was obtained!
The Four Color Problem was first formulated by Francis Guthrie in 1852 when he was coloring a map of the counties of England and noticed that four colors sufficed. He asked his brother Frederick if it was possible to color any map using only four colors while also requiring that adjacent regions (i.e. those sharing a boarder) be of different colors. Frederick, who at this time was a student of Augustus De Morgan, posed the problem to his advisor. De Morgan, in turn, communicated the proposition to his friend William Rowan Hamilton, stating:
“A student of mine 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… “
There were several early attempts to prove this theorem, though all of them failed. The first widely accepted proof was given by Alfred Kempe in 1879, with another proof given independently by Peter Guthrie Tait in 1880. It wasn’t until 11 years later that Kempe’s “proof” was shown to be incorrect by Percy Heawood. 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. In 1891, Tait’s proof was shown to be incorrect by Julius Petersen. Though both early proofs turned out to be fallacious, they were not without value. Kempe discovered what became known as Kempe chains, while Tait found an equivalent formulation of the Four Color Theorem in terms of 3-edge colorings.
During the 1960s and 1970s, German mathematician Heinrich Heesch developed methods using computers to search for a proof. Unfortunately, he was unable to procure the necessary supercomputer time to continue his work. However, others adapted his methods and computer-assisted approach.
The Four Color Theorem was finally proven in 1976 by Kenneth Appel and Wolfgang Haken, with some assistance from John A. Koch on the algorithmic work. This was the first time that a computer was used to aid in the proof of a major theorem. The Appel-Haken proof began as a proof by contradiction. If the Four Color Theorem was false, there would have to be at least one map with the smallest possible number of regions that requires five colors. Two technical concepts were used in the proof:
1. 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.
2. A reducible configuration is an arrangement of countries that cannot occur in a minimal counterexample. That is, if a map contains a reducible configuration, then the map can be reduced to a smaller map (using fewer countries). If this smaller map can be colored using only four colors, then the original (larger) map can also be colored using only four colors. This implies that if the original (larger) map cannot be colored with only four colors, then the smaller map cannot be colored with only four colors either. Thus, the original map could not be a minimal counterexample.
Using mathematical rules and procedures based on the properties of reducible configurations, Appel and Haken found an unavoidable set of reducible configurations, thus proving that a minimal counterexample to the Four Color Theorem could not exist. Instead of examining all possible map configurations (an impossible task), the Appel-Haken proof was able to reduce the problem to looking at a particular set of 1,936 maps. Each of these maps, it was shown, could not be part of a smallest-sized counterexample to the Four Color Theorem. Since checking all of these maps by hand would be tedious and time consuming, Appel and Haken used a special-purpose computer program to confirm that each of the maps had the desired properties. Checking the 1,936 maps one by one took over one thousand computer hours. The reducibility part of this work was independently checked by different programs and different computers. However, the unavoidability portion of the proof needed to be verified by hand, leading to hundreds of pages of analysis. The Appel-Haken proof concluded that no smallest counterexample exists because it must contain, yet cannot contain, one of the specially chosen 1,936 maps. This contradiction shows that there cannot be any counterexamples and therefore the Four Color Theorem must be true.
Initially, this long-awaited proof of the Four Color Theorem was met with trepidation and concern. It was the first major theorem to be proven with extensive computer assistance. In addition, even the human-verifiable portions of the proof were highly complex and prone to error. These two facts caused many mathematicians to reject the proof and led to considerable controversy. In the years that followed the original publication of the proof, it has become more widely accepted, although doubts still remain.
To this day, many mathematicians and philosophers debate whether or not the Appel-Haken proof is legitimate. Some claim that “proofs” should only be accepted if they are proved by people, not machines, while others question the reliability of both the algorithms used and the ability of machines to carry them out without error. Others argue that even proofs written by people can be found to be faulty and so the reliability argument is meaningless. No matter what your opinion on the matter is, the Appel-Haken proof of the Four Color Theorem has led to a serious discussion about the nature of proof which continues today and will continue into the future as we make use of computers that are growing ever more powerful.
Sources:
Appel, Kenneth; Haken, Wolfgang (1989), Every Planar Map is Four-Colorable, Providence, RI: American Mathematical Society, ISBN 0-8218-5103-9
Wilson, Robin (2002), Four Colors Suffice, London: Penguin Books, ISBN 0-691-11533-8
