The Four-Color Theorem is a theorem that has its roots in graph theory. The theorem states that any planar graph can be colored properly with four colors. Here properly colored means that no two vertices of the graph that are connected are colored using the same color. The theorem was first conjectured by F. Guthrie in the year 1852. The conjecture proved to be difficult as the first accepted proof of the theorem was found by Appel and Haken in 1977. This was the first computer assisted proof of a theorem. In this article I will first go over the six and five color theorems to give some intuition into how coloring works. I will finish the article with some insight into the proof of the Four-Color Theorem. 

Planar graphs

To understand the coloring theorem one first needs to know what a planar graph is. A graph is a collection of points (vertices) and lines (edges). A graph can be compared to a network in the sense that different places are connected in some way. An example of a graph can be seen in the figure below.

In a graph, edges can be either directed or undirected. An edge is directed when you can only move between vertices in the given direction of the edge. A graph is called undirected when edges do not have a given direction. In this article we will only consider undirected graphs. Now moving back to the planar graphs, in the simplest sense a graph is called planar if it can be drawn on a flat surface or plane without edges overlapping. The graph above is thus an example of a planar graph as well. Note that a graph being planar is a huge restriction on the edges of the graph. This restriction is what ensures that we can color it using only four colors. Practical examples of planar graphs are maps of the world. Here countries can be seen as the vertices and borders can be seen as edges. 

The Six-Color Theorem

Now that we know what a planar graph is we can start our journey towards the Four-Color Theorem by first proving the Six-Color Theorem. To prove this theorem we rely on the fact that every planar graph has at least one vertex of degree (number of edges incident on a given vertex) at most five. To prove this we need a well known theorem for planar graphs called Euler’s Theorem. This theorem states that . In this equation represents the number of vertices, represents the number of edges and represents the number of faces. A face is a region enclosed by edges. We also call the outside of a graph a face. See the figure below for some more clarification. 

Then we know that each face is enclosed by at least 3 edges. We also know that each edge is incident in enclosing at most 2 faces. Combining these two facts we find that . Now we can rewrite Euler’s Equation to find . Rewriting this again gives us the following inequality: . We also know that the sum of the degrees of a graph is equal to twice the number of edges. This is known as the handshake lemma. This equality implies that 

From this inequality it immediately follows that we cannot have a planar graph where the degree of every vertex is greater or equal to six. So there must be at least one vertex of degree five or lower in every planar graph. See the picture below for a proper coloring of a graph.

Now we are ready to prove the Six-Color Theorem. We first let be a vertex minimal counterexample to the Six-Color Theorem. This means that we need more than six colors to color , but we can color the graph that we obtain by removing any vertex from with at most six colors. Since we know that has a vertex of degree at most five, we remove this vertex from to obtain . We can color with at most six colors. Now when we add back to , we know that is next to at most five colors since its degree is less than or equal to five, meaning that we have a color remaining to color . This implies that can be colored with at most 6 colors which is a contradiction. Hence we have proven that any planar graph can be colored using at most 6 colors. 

The Four-Color Theorem for planar graphs without 3-cycles

The proof for the Four-Color Theorem for planar graphs without 3 cycles is very similar to the Six-Color Theorem. The only difference is that we now have to show that any such graph has a vertex of degree at most 3. We can do this by noticing that each face is enclosed by at least 4 edges if we require the graph not to have any 3-cycles. This means that the inequality we obtain is . Again using Euler’s Equation we can now obtain . Using the same reasoning as before we can conclude that planar graphs without 3-cycles must have a vertex of degree at most 3. Using the vertex minimal counterexample one can prove that the graph is four-colorable with the same argument used as in the proof of the Six-Color Theorem. 

The Five-Color Theorem

For a proof of the Five-Color Theorem we can start similar to the proof of the Six-Color Theorem. Consider a planar graph that is a vertex minimal counterexample to the theorem. Let be a vertex of degree at most five and consider a valid coloring using 5 colors for . If the degree of is less than or equal to 4, we have a color remaining to color and we are done. Thus we only need to consider the case when . We can label the neighbors of as clockwise in a drawing of . We can assume that has color .

First assume that there is no path between and using only the colors 1 and 3. Let us consider the set of points in G that can be reached from only using the colors 1 and 3. If a vertex is adjacent to a vertex in this set it must have a color different from 1 and 3. Otherwise it would be in the set. Because the vertices in the set are only adjacent to colors different from 1 and 3 we can swap the colors 1 and 3 within this set to get a new valid coloring of . In this new coloring and both have the color 3, so we can color with the color 1. Hence we find a valid coloring for .

It remains to consider the case where there is a path between and using only the colors 1 and 3. In this case swapping the colors results in a new coloring where and still have a different color. By the same reasoning there must exist a path between and only using the colors 2 and 4. Now note that the path between and with the vertex forms a cycle that encloses . Thus any path between and must cross the path between and . Since the path between and only consists of the colors 1 and 3 and the path between and only consists of the colors 2 and 4, we have a contradiction. Thus these paths cannot both exist at the same time. Hence we can apply the argument from above to the non-existing path and find a valid coloring of using 5 colors.

The Four-Color Theorem

Now that we have proved the Five-Color Theorem we have arrived at the Four-Color Theorem. The strategy that was used to prove the Four-Color Theorem is similar to that of the Five and Six Color Theorems. You again start with a vertex minimal counterexample and show that such a counterexample does not exist. To show that such a minimal counterexample does not exist, Appel and Haken first show that every planar graph can be reduced to a certain set of subgraphs called configurations. In the proof you consider a minimal counterexample and instead of removing a vertex, you remove a configuration. Then they showed that these configurations could all be colored using four colors using a computer.

Thus they managed to reduce the infinite amount of possible planar graphs to 1,834 reducible configurations. Checking these 1,834 graphs by hand is of course possible, but very time consuming. That is why Appel and Haken enlisted the help of a computer to complete their proof. In 1996 the number of configurations needed was reduced to checking only 633 reducible configurations by Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas. To conclude, with some theoretical proofs the aid of computers is required to check the exhaustive part of the proof and the proof of the Four-Color Theorem was the first example of this. Proofs that are aided by technology are thus far from unthinkable.