A mathematician once told me that problems that are very simple to state can be very deceiving, and sometimes turn out to be extremely difficult to solve. One such problem was the Four Color Problem.
We will take you back to London, it is October of 1852, a remarkably wet autumn according to historic weather archives, with a lot of rainfall, even for English standards. Students probably stayed inside and talked about their studies, worked on problems, and tried to find answers to tantalizing questions.
Francis Guthrie was studying mathematics and botany at the University College London. He was described as a warm-hearted person, good-humored, patient and unpretentious, and with broad interests. Maybe it was on one of those rainy days that he sat on his desk, took a map of the counties of England, and started coloring it. His goal? He wanted to paint all counties using only four colors, such that, any two counties sharing a border would be colored with different colors. Was he curious whether this was possible? Or did he just have four colors available? We will never know. What we know is that on the 23rd of October a mathematical problem was conceived, a problem that would need more than a century to be solved!
Francis succeeded in painting the counties of England using only four colors. Maybe he also noticed that it is not possible to paint the counties using three colors. Maybe he also took other maps and tried to paint all the counties, provinces, or countries in those maps as well, always using only four colors. These are all questions that would trigger a mathematician's curiosity.
In any case, on the 23rd of October, he conjectured that the regions in any map you can think of can be colored using at most four different colors. This conjecture stayed in history as the Four Color Problem, or nowadays known as the Four Color Theorem.
Below the map that Francis Guthrie painted in 1852, can you paint it using only four different colors? What happens if you try with three colors?
A hundred and twenty-four years after it was conceived a definite answer was given to the Four Color Problem. Yes, this conjecture is true! But the discussion was not over yet. Why? Because a computer was used to verify some steps in the proof of the Four Colored Theorem. And many mathematicians didn't like this.
In this article, we will highlight some mile points in the history of this problem, discuss how the problem was solved, and show how computers were used to do some dirty work for us.
A century of efforts
To prove this conjecture mathematicians translated it into a mathematical problem on graphs. This was done as follows, given a map that is divided into regions, we place a vertex inside each region of the map, and draw an edge between two vertices when the corresponding countries share a border. On the map of England, you would then get the following drawing.
The problem of coloring the regions of the map can be translated into a problem of coloring the vertices in the graph. We want to color the vertices with as few colors as possible, such that, no two adjacent vertices have the same color. If you have a coloring of the graph, then you can color the map using the colors of the vertices. Why is this a useful step? Well, you can now just ignore the map and look only at the graph!
The graph that we have obtained has an amazing property, it is planar. A graph is called planar if it can be drawn on a piece of paper without crossing edges. Since borders do not cross each other, every map corresponds to a planar graph. Vice versa, every planar graph can be considered as a map of (imaginary) countries.
The Four-Color Theorem states that the chromatic number, i.e. the least number of colors needed to color a graph such that vertices sharing an edge don't have the same color, of any planar graph is less or equal to four. Consequently if someone can prove this mathematical statement on planar graphs, then you have shown that any map can be colored using four colors.
Four Color Problem on maps
In any map possible, all the regions can be colored using at most four colors. Two regions sharing a border never have the same color.
Graph theory problem
Any planar graph has chromatic number less or equal to four.
There were several early failed attempts at proving the Four-Color Theorem. The most famous proof was given by Alfred Kempe in 1879, and it was not until 1890 that Kempe’s proof was shown incorrect by Percy Heawood. In addition to exposing the flaw in Kempe’s proof, Heawood proved the Five Color theorem, which states that every planar graph can be colored with five colors (on Wikipedia you can find a nice argument about this result). Almost there, we just need to remove one of the five colors!
Many concepts in modern graph theory, for example, the chromatic polynomial, were invented in an attempt on proving the Four Color Theorem. During the 1960s and 1970s, German mathematician Heinrich Heesch developed methods using computers to search for a proof.
Notably, he was the first to use a mathematical technique called the Discharging Method in trying to prove the theorem. Others took up his methods, and on June 21, 1976, Kenneth Appel and Wolfgang Haken announced that they had proven the Four Color Theorem using the Discharging Method. A hundred and twenty-four years had passed from that rainy night this problem was conceived by Francis Guthrie, and finally an answer has been found.
In the follow up, we globally discuss which were the main ideas behind the proof of the Four Color Theorem, and discuss in more detail, but without technicalities, how the Discharging Method works.
A well desired proof
In the proof of the Four Color Theorem, some important mathematical techniques were used. To start with, it is a proof using a contradiction. A proof by contradiction goes as follows, you want to prove statement A, then you suppose that statement A is not true, and then after well-chosen logical steps, you deduce that this would lead to a contradiction. Hence statement A has to be true.
Mathematicians supposed that the Four Color Theorem is not true and tried to see what the implications would be, hoping to find a contradiction. If the theorem is not true then there has to exist at least one planar graph that has chromatic number at least equal to 5. Such a graph would need at least 5 colors to be painted.
The next step is to consider the minimal planar graph that is not colorable using 4 colors. This is the graph that has the least amount of vertices among all planar graphs that are not 4-colorable. Such a minimal graph is called is a minimal counterexample. The general idea of the proof is to try and show that if such a minimal counterexample would exist then you can make a smaller graph out of it which would still not be colorable, which obviously forms a contradiction since we started with a minimal counterexample! Contradictions can be mind-stretching sometimes, but they are legit and also quite fun to think about.
The road to the contradiction
Let's start from the minimal counterexample we discussed above. This is a graph that is not 4-colorable and has the least amount of vertices among all graphs that are not 4-colorable. The next step is to find some necessary conditions this minimal counterexample has to satisfy. The nature of the necessary conditions found for the Four Color Theorem is quite technical and we will not describe them here, however, this step can still be done using only pen and paper. No computers are needed yet.
The following milestone in the proof is to find a so-called set of unavoidable configurations. This is a list of smaller graphs, such that, every graph that satisfies the necessary conditions and is not 4-colorable must contain at least one graph from this list. Hence also the minimal counterexample has to contain at least one of these unavoidable configurations. Until now you must start feeling this solution to the Four Colored Theorem is very complex. Moreover, making sure that all arguments are air-tight was a very cumbersome endeavor.
This list of unavoidable configurations has a second astonishing property. The first property was that the minimal counterexample must contain at least one graph from this list. The second property is that using this configuration the minimal counterexample can be reduced to a smaller graph, which has to be 4-colorable, since it is smaller than the minimal counterexample, and whose 4-coloring can be extended to a 4-coloring of the minimal counterexample! Which is a contradiction, since we supposed at the beginning that the minimal counterexample cannot be colored using only 4 colors! Mind stretching right? Combining these two facts yields a proof of the Four Color Theorem! In the following section we are going to discuss in more detail the Discharging Method, which was used to find the list of unavoidable configurations.
Charging and Discharging a Graph
The best-known list of unavoidable configurations consists of 633 graphs and was found using the Discharging Method. But how does the Discharging Method actually work?
The Discharging method is a proof technique in graph theory that is used to prove that every graph in a certain class must contain some subgraph from a specified list. The presence of the desired subgraph is then often used to prove a coloring result. In general, the Discharging Method relies on two steps, a charging phase, and a discharging phase.
In the charging phase we undertake two actions, namely:
we assign an initial charge (some numerical value) to certain elements of a graph (vertices, edges, faces, etc.) and
we compute the total charge assigned to the whole graph.
An example of such an initial charge is the following: we assign an initial charge of +1 to all vertices and faces of a graph, and an initial charge of −1 to all edges. This is shown in the figure below.
Figure 1: Charging rule: we assign an initial charge of +1 to all vertices and faces of a graph, and an initial charge of −1 to all edges.
The discharging phase follows and the following two actions are taken:
we redistribute the charges in the graph according to a set of discharging rules. It is important that no additional charge is introduced or lost.
Finally, we compute the final charges and derive a conclusion.
In the graph with the initial charges shown above we can, for example, define the following discharging rule: each vertex and each edge gives all its charge to the face immediately to its right. This discharging rule is shown below.
Figure 2: Discharging rule: each vertex and each edge gives all its charge to the face immediately to its right. Blue means that the charge goes to the inner face, red that it goes to the outer face.
You can try it yourself as a puzzle, what will the new charges of the vertices, the edges, and the faces become?
If you work it out you will find that the final charges of the vertices and the edges are 0. The final charge of all inner faces will also become 0 and only the outer face will have a charge equal to 2. So in this specific graph, you obtain that only the outer face will have a positive charge equal to 2 after the discharging phase.If we push this puzzle one step further you can actually show much more, you can reason that in any planar graph, the result of the discharging phase will be that only the outer face remains with a positive charge equal to 2. Do you see why?
Let's see why this happens. The vertices and edges immediately to the left of an inner face (blue arrows in Figure 2) will always form a sequence of alternating vertices and edges, whose two endpoints are vertices that give their charge to another face. Thus, the number of vertices immediately to the left of an inner face will always be one less than the number of edges. It follows that the final charge of any inner face is 0. The vertices and edges on the right side of the graph (red arrows on the right-hand side in Figure 2) always form a sequence of alternating vertices and edges, whose two endpoints are vertices giving a +1 charge to the outer face. All other red vertices cancel against a red edge. Thus the charge of the outer face goes up by 1.
But what did we achieve by doing all of this? Let's collect all our results. We had a graph and we assigned charges to all the vertices, edges, and faces according to a charging rule. Afterward, we redistributed the charges according to a discharging rule which didn't affect the total charge. Hence let's have a look at the total charge on the graph. On the graph after discharging it is easy to compute the total charge, it is equal to 2.
It is more challenging to compute the total charge in the graph before discharging. Each vertex and face had a charge equal to +1, each edge equal to -1. Hence the total charge is equal to, . Here represent the total amount of vertices, edges, and faces in the graph respectively.
Combining these two results we obtain the equation
which is known as Euler's formula! Euler’s formula states thus that the number of vertices minus the number of edge plus the number of faces in a planar graph is always equal to two.
Back to the colors
To prove the Four-Color Theorem, the Discharging Method is used to find an unavoidable list of configurations. Computers were used in this step. It can also be carried without using computers, but it would take a full month to verify it, while it takes only a few minutes for a computer.
Kenneth Appel and Wolfgang Haken used 487 discharging rules to find a list of 1834 (later reduced to 1482) graphs which are unavoidable. Later, Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas used 32 discharging rules to find a list of 633 unavoidable graphs.
One of the smallest graphs in this list is the Birkhoff's Diamond, shown in the figure below.
Birkhoff's Diamond
As a puzzle, you can show that Birkhoff's number has chromatic number equal to 4, i.e., to color all the vertices so that no adjacent vertices have the same color, you need 4 colors or more.
The final blow
The final step of the proof consists of checking that every graph in the list of unavoidable configurations cannot occur in a minimal counterexample. If the minimal counterexample contains a graph from the list, we can reduce it to a smaller graph that can be colored with four colors, since the counterexample was minimal.
Computers were used to show that the 4-coloring of the smaller graphs, obtained after removing a graph from the list, can be extended to a 4 coloring of the minimal counterexample, which is a contradiction as the minimal counterexample was not 4-colorable!
This finalizes the proof because the minimal counterexample must contain a graph from the list of unavoidable configurations, but at the same time, it cannot contain these graphs since if it would we could find a 4-coloring of it. Hence a minimal counterexample cannot exist!
Maybe when you started reading this article you were expecting a very elegant argument showing that every planar graph is 4-colorable. Perhaps now after finishing this article you will doubt it. After reading this article you must be convinced that coming up with this proof was a very cumbersome procedure, that required a lot of patience and meticulous computations. All means possible were used to prove this - very simple to state - problem. But the problem is settled.
The Four-Color Theorem was the first major theorem to be proved by a computer. Therefore the proof was not accepted by all mathematicians, because it was practically impossible to check it by hand. Nowadays, there are more computer-assisted proofs in mathematics.
Also, the proof of the Four-Color Theorem is widely accepted, even though it still cannot be proven by hand. Maybe a more elegant argument will be found to prove it in the future. In any case, the persistence of the mathematicians who worked in proving this theorem is remarkable.
On Wednesday I was teaching an exercise class on graph theory. There was this one exercise that was troubling me for a couple of days, I couldn't solve it and it was frustrating.
Recently there has been a breakthrough in the field of algorithms for geometric network problems, concerning the complexity of the Euclidean Travelling Salesman Problem.
Ever wondered how stolen necklaces are tactfully divided? Join us on a captivating journey into the math under necklace splitting! This journey will lead us to a wonderful and very important theorem in mathematics, the Borsuk-Ulam theorem.
In times of war, secure communication can be the difference between life and death, or even winning or losing a war. The first to patent a rotor machine in Europe was Arthur Scherbius in 1918. Scherbius’ version of the rotor machine became a commercial success, unlike the other patented machines. Scherbius named his machine Enigma.
