With an amusing history spanning over 150 years, the four color problem is one of the most famous problems in mathematics and computer science. The four color theorem states that the regions of a map (a plane separated into contiguous regions) can be marked with four colors in such a way that regions sharing a border are different colors.
An origin story
Normally omitted from histories of the four color problem is a report by geometer Richard Baltzer about a “coloring problem” from one of Möbius‘s lectures. Baltzer claimed that Möbius heard the following story from philologist Benjamin Gotthold Weiske, and then delivered it in a geometry lecture:
Once upon a time, a king in India had a large kingdom and five sons. His last will and testament decreed that, after his death, the sons should partition the kingdom in such a way that each one’s region would have a common boundary (not just a single point) with each other’s regions. How was one to divide the kingdoms?
Moving forward, the four color problem is accredited to Francis Guthrie in 1852. The origin is exactly as one would imagine: Guthrie was coloring a map of the counties of England and thought it was helpful to color counties that neighbored each other differently. He soon realized that three colors were not enough, but four colors were. Guthrie wondered if four colors suffice for any map.
The problem travels
Francis passed the problem onto his brother, Frederick Guthrie, who was a student at University College. From there, the problem landed in the hands of some very famous mathematicians including Augustus De Morgan, William Rowan Hamilton, and Arthur Cayley.
De Morgan first thought the problem must have an easy solution that he was missing. In a letter to Hamilton, he wrote:
If you retort with some very simple case which makes me out a stupid animal, I think I must do as the Sphynx did.
To this, Hamilton responded condescendingly and acted as though the problem were beneath him. In 1880, both Peter Guthrie Tait and Alfred Kempe published different “proofs” for the four color problem which were thought to be correct for about ten years, until they were both separately disproven. Although, Kempe’s failed attempt did lead to a valid proof that five colors suffice, and the proof is very easy if you haven’t seen it! Progress on the four color problem was slow and spotty for the next several decades, but techniques used to chip away at the four color problem increased the popularity of a branch of mathematics called graph theory (to be discussed more soon).
Reformulating the problem
The key to moving forward on the four color problem was reshaping the theorem from a universal statement to an existential statement. Instead of considering: can every map be colored with only four colors, mathematicians wondered does there exist a small map which needs five colors. If the four color theorem were not true, there would exist a map with the smallest number of regions which requires five colors. This map is referred to as the minimum counterexample.
A configuration is an arrangement of regions in a map. An unavoidable set is a set of configurations such that every map contains at least one of the configurations from the unavoidable set; so it is unavoidable that every map contains an arrangement from the unavoidable set. If a map contains a reducible configuration, then the map can be reduced to a map with fewer regions so that if the smaller map can be colored with four colors then so can the bigger map.
This means that if the minimum counterexample contains a reducible configuration, then its reduced map can also not be colored with four colors. But the reduced map has fewer regions that the original map, so it must be that the minimum counterexample cannot contain a reducible configuration. In the early 1900s, American mathematicians reformulated the four color problem to be finding an unavoidable set of reducible configurations. This would prove that the minimum counterexample does not exist.
Aside: graph theory
The four color problem is discussed using terms in graph theory, the study graphs. A graph is a set of vertices, where a pair of vertices are connected with an edge if some relation holds between the two. The four color problem is examined in graph theory, where the vertex set is the regions of a map and an edge connects two vertices exactly when they share a border. Additionally, the graphs under consideration are planar.
Planar graphs can be drawn in such a way that no edges cross each other outside the endpoints. Excluding that cute story told in Möbius’s lecture, the four color problem was the first recorded coloring problem, which is a class of problems where vertices are assigned colors (or some other label) subject to certain constraints.
Heinrich Heesch was a German mathematician who established a set of discharging rules to try and find an unavoidable set. In a discharging method, a charge is assigned to each vertex and face (the regions created from the edges in a graph). The original assignments of charges are made to sum to a small positive number. Then, the charges at the faces and vertices are redistributed according to a set of discharging rules, but the total sum of the charges remains the same. A discharging method is used to prove that every graph in a certain class contains a subgraph from some other set. Given the right set of discharging rules and unavoidable set, it could be used to prove that every map contains a configuration from an unavoidable set
In 1976 at UIUC, Kenneth Appel and Wolfgang Haken proved that no minimum counterexample exists, which proved the four color theorem. The team found an unavoidable set of 1,936 reducible configurations. Then, they checked that all of these were four colorable using a dynamic programming algorithm. The use of dynamic programming allows for a configuration which is proven to be four colorable to be used to prove that other configurations are four colorable.
The four color theorem was the first major theorem to be proved using a computer. The reducibility portion of Appel and Haken’s proof was checked with computer, while the unavoidability part used a discharging method and was checked by hand. There were some slight misunderstandings and misprints found in their original release, but modulo these, Appel and Haken’s proof was correct. In 1996, a group of mathematicians, including Robin Thomas and Paul Seymour, created an algorithm which can properly four color a map in quadratic time (given n regions to color, the algorithm takes O(n²) steps). They did this by using only 633 of the reducible configurations.
Computer proofs have progressed beyond exhaustive search, which is neither elegant nor provides intuition on a problem. Advancements in artificial intelligence in the 1950s allowed computer scientists to begin working to better understand and imitate how humans reason, which became known as automated reasoning. Within this intersection of computer science and mathematical logic, proof assistants were developed. Proof assistants, or interactive theorem provers, are software tools which check mathematical claims and help find formal proofs with interaction from the user. A proof of the four color theorem was formalized inside the Coq proof assistant by Benjamin Werner and Georges Gonthier in 2005. It’s considered a more reliable proof because it removed the weakest aspects of Appel and Haken’s argument.
What is a proof? (to be continued)
Proofs of the four color theorem were not entirely well-received by the mathematics community. When Appel and Haken’s proof was first presented publicly, it was actually met with some hostility and incredulity.
Paul Erdös nicely explained why many mathematicians were at least disappointed:
I’m not an expert on the four color problem, but I assume the proof is true. However, it’s not beautiful. I’d prefer to see a proof that gives insight into why four colors are sufficient.