The Four Color Theorem: Why Maps Need Four Colors, and the First Proof Written by a Computer

0. Key points

• Every map drawn in the plane can be colored with four colors in such a way that adjacent countries receive different colors. This is the four color theorem.
• Translating “map” into “planar graph” turns the question into “can the vertices of a planar graph be colored with four colors?” — a question about points and lines rather than about pictures.
• Euler’s formula yields the statement that every planar graph has a vertex of degree at most 5, and from there the six-color theorem follows almost automatically, while the five-color theorem follows using a tool called a Kempe chain. Up to this point the work takes an hour with pencil and paper.
• But the last step, from 5 down to 4, is strangely rigid. In 1976 Appel and Haken finally settled it by checking some 1900 “configurations” by computer. It was the first major theorem whose full proof no human being could read.
• In 1997 the proof was substantially simplified, and in 2005 it was completely formalized in the proof assistant Coq. The question “may we trust a computer’s proof?” has by now turned into the more concrete question “which pieces of software do we trust, and how far?”

1. Motivation: a problem that began with coloring an atlas

In 1852 Francis Guthrie, a student in London, was coloring a map of the English counties when he noticed something. He wanted adjacent counties to get different colors, and however he went about it four colors always sufficed. Try as he might to construct a map forcing a fifth color, somehow he could not.

He passed the question to his brother Frederick, then a student of the mathematician De Morgan, and Frederick put it to his supervisor. On 23 October of that same year De Morgan described the problem in a letter to Hamilton. That is the recorded birthday of the four color problem.

The question is intelligible to a child.

Given a map in the plane, how many colors suffice to color it so that any two countries sharing a border receive different colors?

On the “sufficient” side the answer is four. The “necessary” side — that there exist maps for which fewer than four colors will not do — is verified in Example 2.3 just below. So the answer is exactly 4.

What deserves attention here is that the difficulty of this problem is nowhere visible. Its statement mentions neither derivatives nor infinity. Nevertheless it took 124 years to settle, and the manner of its settlement caused a small commotion in the mathematical world. In being a simple question of frightening depth, it belongs to the same species as the Collatz conjecture — in particular to problems such as the Collatz map（Definition 2.1）［The Collatz Conjecture］ whose definition takes only a few lines.

Note

No short, intuitive reason for the number 4 is known at present. As we shall see, for six colors and for five colors the reason can be laid out cleanly. Only that last color’s worth of the statement keeps refusing to explain itself.

2. Preliminaries: translating maps into graphs

2.1. What is a map?

Let us first fix the word “map” in mathematical language. Vagueness here makes the theorem false, so we proceed carefully.

Definition 2.1（Maps and colorings）

A map is a division of the plane into finitely many regions $R_1, \ldots, R_n$, called countries. Each country $R_i$ is required to be a connected open set whose boundary consists of finitely many curves. Two countries $R_i, R_j$ are adjacent if their boundaries have a part in common and that common part is not a single point but contains a curve.

A function $c \colon \{R_1,\ldots,R_n\} \to \{1,\ldots,k\}$ is a $k$-coloring if $c(R_i) \neq c(R_j)$ holds for every pair of adjacent countries $R_i, R_j$.

Two conditions are doing work here.

(a) Countries are connected. Allowing exclaves destroys the theorem (Example 2.4).

(b) Meeting at a single point does not count as adjacency. A pie chart, in which many countries come together at the center, makes this clear. If countries meeting at a single point were counted as adjacent, then a disc cut into $n$ sectors would already require $n$ colors, and again the theorem would fail. We are simply adopting the everyday view that a border is a line and not a point.

2.2. The dual graph

Maps are awkward to handle as they stand, so we translate them into points and lines. Place one “capital” inside each country and join the capitals of two adjacent countries by a line crossing their common border. The figure so obtained is called the dual graph.

A map (left) and its dual graph (right). The small central country D touches each of A, B, C, and A, B, C touch one another, so the dual graph is the complete graph K4 on four vertices.

What matters is that this dual graph can be drawn in the plane. Each of the joining lines crosses a border exactly once, so they can be drawn without meeting one another. The problem has now been translated completely.

Definition 2.2（Planar graphs and their colorings）

A graph $G = (V, E)$ consists of a finite vertex set $V$ together with a set $E$ of edges, each of which is a two-element subset of $V$. All graphs in this article are simple: no loops and no multiple edges. The number of edges incident with a vertex $v$ is the degree of $v$, written $\deg(v)$.

$G$ is a planar graph if it can be drawn by assigning its vertices to distinct points of the plane and its edges to curves joining their endpoints, in such a way that no two edges meet except at a common endpoint. A particular such drawing, once fixed, is called a plane drawing.

A function $c \colon V \to \{1,\ldots,k\}$ is a $k$-coloring of $G$ if $c(u) \neq c(v)$ holds for every two vertices joined by an edge $\{u,v\} \in E$. The smallest $k$ for which a $k$-coloring exists is the chromatic number $\chi(G)$ of $G$.

Degrees and the rudiments of planar graphs are also introduced in degree and Eulerian trails（Definition 5.1）［Euler and Ramanujan］ and planar graphs（Definition 5.4）［Euler and Ramanujan］.

From here on everything said about maps is carried out in this language. What we wish to show is: if $G$ is a planar graph then $\chi(G) \le 4$.

Example 2.3（A map that really does need four colors）

We use the map in the figure above as it stands. The countries A, B, C are arranged in a ring and are pairwise adjacent, and the central country D is adjacent to all of A, B, C. Hence in the dual graph every two of the four vertices are joined by an edge; this graph is denoted $K_4$.

Suppose three colors sufficed. Since A, B, C are pairwise adjacent, the values $c(A), c(B), c(C)$ are three distinct colors and exhaust $\{1,2,3\}$. As D is adjacent to all three countries, $c(D)$ must differ from each of $1, 2, 3$, and no candidate is left in $\{1,2,3\}$. Contradiction. Hence $\chi(K_4) = 4$, and this map does require four colors.

“Four colors suffice” is the theorem; “four colors are necessary” is finished by this single example. It is always the sufficiency side that is hard.

Example 2.4（Allowing exclaves makes the number of colors needed arbitrarily large）

Let us see what happens if condition (a) of Definition 2.1 is dropped. Take $n$ countries $C_1, \ldots, C_n$ and give each of them one “mainland” piece together with $n-1$ “exclave” pieces. Along the top, place tall rectangles (the mainlands) $C_1, C_2, \ldots, C_n$ from left to right, and draw a horizontal border along their lower edges.

In the bottom row, subdivide the strip lying directly beneath the mainland $C_j$ into $n-1$ small rectangles side by side, and place in them one exclave of each country $C_i$ with $i \ne j$. Then $C_i$ shares a stretch of border with every mainland $C_j$, $j \ne i$, by way of its own exclave placed directly below it. Every pair $(C_i, C_j)$ with $i \ne j$ is adjacent, so $n$ colors are needed. Taking $n = 100$ we need 100 colors.

This shows that the four color theorem depends utterly on the seemingly innocuous condition that countries be connected. To a real-world map containing a country with an exclave — a world map including the Russian oblast of Kaliningrad, say — the theorem does not apply as it stands.

3. First, the six-color theorem

Four is out of reach at once, so we begin with six. The only tool we use here is Euler’s formula (Euler's polyhedron theorem（Theorem 5.5）［Euler and Ramanujan］).

Proposition 3.1（Euler's polyhedron formula）

Let a connected planar graph be given together with a plane drawing of it. Write $V$ for the number of vertices, $E$ for the number of edges, and $F$ for the number of regions into which the drawing divides the plane (the faces, the unbounded outer region being counted as one of them). Then

$$V - E + F = 2 .$$

Proof（Proposition 3.1）

We argue by induction on the number of edges $E$.

Base case: $E = 0$. By connectedness there is a single vertex, and there is a single face, the whole plane. Then $V - E + F = 1 - 0 + 1 = 2$, as required.

Induction step: let $E \ge 1$ and assume the formula for every connected plane drawing with at most $E - 1$ edges. We distinguish two cases.

(i) $G$ contains a cycle. Choose an edge $e$ lying on such a cycle. Since $e$ is on a cycle, deleting it preserves connectedness. Moreover, by the Jordan curve theorem the cycle separates the plane into an inside and an outside, so the two sides of $e$ belong to two distinct faces. Deleting $e$ merges these two faces into one. Hence $V' = V,\ E' = E-1,\ F' = F-1$, and the induction hypothesis gives $V' - E' + F' = 2$, that is $V - (E-1) + (F-1) = 2$, which is equivalent to $V - E + F = 2$.

(ii) $G$ contains no cycle. Being connected and acyclic, $G$ is a tree, and a tree has a vertex of degree 1 (a leaf). Deleting a leaf $v$ together with its incident edge $e$ leaves a connected tree. The two sides of $e$ lie in the same face, so the number of faces does not change. Hence $V' = V-1,\ E' = E-1,\ F' = F$, and the induction hypothesis gives $(V-1) - (E-1) + F = 2$, that is $V - E + F = 2$.

In either case the formula follows.

∎

Example 3.2（Checking the formula on the cube）

Consider the graph formed by the 8 vertices and 12 edges of a cube. Flattening the cube into the plane, as though peering into it through one of its faces, gives a large square containing a small square with corresponding corners joined. No two edges cross in this picture, so it is a plane drawing.

Counting faces: the four trapezoids between the large and the small square, the inner small square, and the region outside the whole figure, so $4 + 1 + 1 = 6$. Indeed

$$V - E + F = 8 - 12 + 6 = 2 ,$$

so Proposition 3.1 holds. That this agrees with the six faces of the cube as a solid is no accident either: when we flattened it, the face nearest to us turned into the unbounded outer region.

Euler’s formula imposes on planar graphs the restriction that they cannot have too many edges. This is the key to everything that follows.

Lemma 3.3（Upper bound on the number of edges of a planar graph）

Let $G$ be a simple planar graph with $V \ge 3$ vertices. Then its number of edges $E$ satisfies

$$E \le 3V - 6 .$$

Proof（Lemma 3.3）

We first treat the case where $G$ is connected. Fix a plane drawing of $G$ and let $F$ be the number of faces.

For each face consider the length of the closed walk that traverses its boundary once (the boundary walk). Since $G$ is simple, connected and has $V \ge 3$, every boundary walk has length at least 3. Indeed, length 1 would require a loop and length 2 a multiple edge, and a simple graph has neither. A boundary walk of length 2 could also arise by traversing a single edge back and forth, but that happens only when $V = 2$ and there is just one edge, contradicting the assumption that $V \ge 3$ and $G$ is connected.

On the other hand every edge occurs exactly twice among the boundary walks (once in each of the two faces on its sides when these differ, and twice in the same face when they coincide). Summing the lengths of the boundary walks over all faces therefore gives the total number of occurrences of edges, which is $2E$. Hence

$$2E = \sum_{f} (\text{length of the boundary walk of the face } f) \ge 3F ,$$

that is $F \le \frac{2}{3}E$. Substituting this into $F = 2 - V + E$, which comes from Proposition 3.1, gives

$$2 - V + E \le \tfrac{2}{3}E ,$$

and subtracting $\frac{2}{3}E$ from both sides and rearranging yields $\frac{1}{3}E \le V - 2$, that is $E \le 3V - 6$.

If $G$ is not connected, we may add edges between distinct connected components while keeping the plane drawing (the components are separated in the plane, so an edge can be routed through the outer face). Adding edges preserves both planarity and simplicity, so applying the above to the resulting connected graph $G'$ gives $E \le E(G') \le 3V - 6$.

∎

Corollary 3.4（Existence of a vertex of small degree）

Every simple planar graph $G$ has at least one vertex of degree at most 5.

Proof（Corollary 3.4）

Let $V$ be the number of vertices. If $V \le 6$, then every degree in a simple graph is at most $V - 1 \le 5$ and the claim is immediate. So assume $V \ge 7$ (in particular $V \ge 3$).

Suppose every vertex had degree at least 6. By the handshake lemma (each edge contributes 1 to each of the degrees of its two endpoints),

$$2E = \sum_{v} \deg(v) \ge 6V ,$$

so $E \ge 3V$. But Lemma 3.3 gives $E \le 3V - 6$, whence $3V \le E \le 3V - 6$ and therefore $0 \le -6$, a contradiction. Hence a vertex of degree at most 5 exists.

∎

Theorem 3.5（Six-color theorem）

Every simple planar graph $G$ satisfies $\chi(G) \le 6$. That is, every map in the plane can be colored with six colors.

Proof（Theorem 3.5）

We argue by induction on the number of vertices $V$.

Base case: if $V \le 6$, assigning a separate color to each vertex uses at most six colors.

Induction step: let $V \ge 7$ and assume that every simple planar graph with at most $V-1$ vertices has a 6-coloring. By Corollary 3.4 we may take a vertex $v$ with $\deg(v) \le 5$. Deleting $v$ together with all edges incident with it gives a graph $G - v$, a simple planar graph on $V-1$ vertices (subgraphs of planar graphs are planar). By the induction hypothesis $G - v$ has a 6-coloring $c$.

The vertex $v$ has at most 5 neighbors, so they use at most 5 of the colors. At least one of the six colors is therefore absent from the neighborhood of $v$. Taking that color as $c(v)$ makes the colors differ along every edge incident with $v$, and we obtain a 6-coloring of the whole of $G$.

∎

Looking back at the proof, the only thing doing any work is the statement that a vertex of degree at most 5 must exist. Remove such a vertex to make the graph smaller, and when putting it back make sure a color is left over. If we keep six colors in reserve for a vertex of degree at most 5, one is bound to remain. It is a remarkably cheap argument.

4. Kempe chains and the five-color theorem

Six colors were too easy. With five, the argument above breaks down at exactly one place: when we delete a vertex of degree 5 and put it back, its five neighbors may have used up all five colors, leaving nothing over.

This is where a tool introduced by Alfred Bray Kempe in 1879 enters. With it he “proved” the four color theorem, and for eleven years the proof was believed. In 1890 Percy John Heawood found the error — but at the same time showed that the argument does go through for five colors. One genuine theorem was salvaged from a broken proof.

Definition 4.1（Kempe chains）

Let a coloring $c$ of $G$ and two colors $i, j$ be given. Write $H_{i,j}$ for the subgraph induced by all vertices whose color is $i$ or $j$. Each connected component of $H_{i,j}$ is called an $(i,j)$-Kempe chain with respect to $c$.

Kempe chains are useful because of the following property: they let us rearrange a coloring locally, so that an inconvenient arrangement of colors can be replaced by a convenient one.

Lemma 4.2（Swapping along a Kempe chain）

Let $c$ be a coloring of a simple graph $G$ and let $K$ be an $(i,j)$-Kempe chain with respect to $c$. Interchange the colors $i$ and $j$ at the vertices belonging to $K$ only, leaving the colors of all vertices outside $K$ unchanged. The resulting function $c'$ is again a coloring of $G$.

Proof（Lemma 4.2）

Take an arbitrary edge $\{u,w\} \in E$ and check that $c'(u) \ne c'(w)$. There are three cases, according to whether $u$ and $w$ lie in $K$.

(1) Both $u$ and $w$ lie in $K$. Then $c(u) \ne c(w)$ and both colors are $i$ or $j$, so $\{c(u), c(w)\} = \{i, j\}$. After the interchange $c'(u)$ and $c'(w)$ again take the values $i$ and $j$, one each, hence differ.

(2) Both $u$ and $w$ lie outside $K$. Neither color changes, so $c'(u) = c(u) \ne c(w) = c'(w)$.

(3) $u \in K$ and $w \notin K$. The color of $u$ is $i$ or $j$. If the color of $w$ were also $i$ or $j$, then $w$ would be a vertex of $H_{i,j}$ joined to $u$ by an edge, hence in the same connected component as $u$, that is in $K$, contrary to assumption. So $c(w)$ is neither $i$ nor $j$. Since $c'(u)$ is $i$ or $j$, we get $c'(u) \ne c(w) = c'(w)$.

Thus the colors differ along every edge, and $c'$ is a coloring.

∎

Theorem 4.3（Five-color theorem）

Every simple planar graph $G$ satisfies $\chi(G) \le 5$.

Proof（Theorem 4.3）

We argue by induction on the number of vertices $V$. If $V \le 5$, give every vertex a different color. So let $V \ge 6$ and assume that a 5-coloring exists for every such graph on at most $V-1$ vertices.

By Corollary 3.4 take a vertex $v$ with $\deg(v) \le 5$, and fix a plane drawing of $G$. Since $G - v$ is a simple planar graph on $V-1$ vertices, the induction hypothesis provides a 5-coloring $c$ of it.

If the neighbors of $v$ use at most 4 colors, we are done: take the leftover color as $c(v)$ (the case $\deg(v) \le 4$ falls under this automatically). So the only remaining situation is $\deg(v) = 5$ with the five neighbors using all five colors.

In the plane drawing, list the five edges leaving $v$ in the cyclic order in which they occur around $v$, and let $v_1, v_2, v_3, v_4, v_5$ be the vertices at their far ends in that order. Renaming the colors we may assume $c(v_k) = k$ for $k = 1,\ldots,5$.

Case 1: $v_1$ and $v_3$ lie in different connected components of $H_{1,3}$. Interchange the colors 1 and 3 inside the Kempe chain containing $v_1$ only. By Lemma 4.2 this is still a 5-coloring of $G - v$. Since $v_3$ does not belong to that chain, it retains color 3, while $v_1$ has changed to color 3. So the neighbors of $v$ now carry the colors $3, 2, 3, 4, 5$, and color 1 occurs nowhere among them. Setting $c(v) = 1$ completes a 5-coloring of $G$.

Case 2: $v_1$ and $v_3$ lie in the same connected component of $H_{1,3}$. Then there is a path $P$ from $v_1$ to $v_3$ passing only through vertices colored 1 and 3. Adding to $P$ the edges $v v_1$ and $v_3 v$ produces a closed curve $C$ inside the plane drawing.

By the Jordan curve theorem, $C$ divides the plane into an inside and an outside. Since the cyclic order around $v$ is $v_1, v_2, v_3, v_4, v_5$, the vertex $v_2$ lies on one side of $C$ and $v_4$ on the other ($v_2$ lies in the sector between $v_1$ and $v_3$, while $v_4$ lies in the sector joining $v_3$ back to $v_1$ the other way round).

Now suppose $v_2$ and $v_4$ lay in the same connected component of $H_{2,4}$. Then there would be a path $Q$ from $v_2$ to $v_4$ passing only through vertices colored 2 and 4. Since $Q$ crosses from the inside of $C$ to the outside, in the plane drawing it would have to meet $C$. But two edges meet only at a common endpoint, so the meeting would have to be at a shared vertex. The vertices on $C$ are $v$ and vertices colored 1 or 3, whereas the vertices on $Q$ are colored 2 or 4, so the colors cannot agree; and $v$ is not on $Q$ since $v$ does not belong to $G - v$. There is no way for them to meet, a contradiction.

Hence $v_2$ and $v_4$ lie in different components of $H_{2,4}$. Interchanging the colors 2 and 4 in the Kempe chain containing $v_2$ turns the color of $v_2$ into 4 while $v_4$ stays 4. The neighbors of $v$ then carry the colors $1, 4, 3, 4, 5$, and color 2 is free. Setting $c(v) = 2$ gives a 5-coloring of $G$.

In both cases a 5-coloring can be constructed, and the induction is complete.

∎

Remark 4.4（Where Kempe went wrong）

In 1879 Kempe asserted four colors within the same framework. With four colors, deleting a vertex $v$ of degree 5 leaves five neighbors and only four colors, so some color must be repeated. Splitting into cases according to the repetition, one is left at the end with a situation requiring two Kempe chains to be interchanged simultaneously. Kempe took it for granted that this could be done.

But when two chains are entangled, interchanging along one of them can alter the shape of the other, so that the second interchange is no longer legitimate. In 1890 Heawood exhibited precisely this by constructing a map with 25 countries in which it happens. That the proof of Theorem 4.3 above performs only one interchange is no coincidence. One interchange is enough for five colors, two are needed for four, and that difference amounted to 86 years of difficulty.

Example 4.5（Coloring from one end in order does not reach four）

Let us see how unreliable the naive strategy of “color the vertices of small degree first” (greedy coloring) can be.

Take six vertices $a_1, a_2, a_3, b_1, b_2, b_3$ and join $a_i$ to $b_j$ exactly when $i \ne j$. This graph with 6 vertices and 6 edges is the cycle $a_1 b_2 a_3 b_1 a_2 b_3 a_1$ of length 6, and it can be drawn in the plane. Coloring the $a$‘s one way and the $b$‘s the other, two colors suffice.

But if we list the vertices in the order $a_1, b_1, a_2, b_2, a_3, b_3$ and assign to each in turn the smallest color not yet used on its neighbors, we get the following.

Step	Vertex	Neighbors already colored	Color assigned
1	$a_1$	none	1
2	$b_1$	none (the neighbors of $b_1$ are $a_2, a_3$)	1
3	$a_2$	$b_1$ (color 1)	2
4	$b_2$	$a_1$ (color 1)	2
5	$a_3$	$b_1$ (1), $b_2$ (2)	3
6	$b_3$	$a_1$ (1), $a_2$ (2)	3

We have used three colors on a graph that needs only two. Extending the same construction to $n$ pairs makes the greedy method use $n$ colors. Coloring is not something that can be controlled by proceeding in order.

5. From five to four: unavoidable sets and reducible configurations

Theorem 5.1（Four-color theorem）

Every simple planar graph $G$ satisfies $\chi(G) \le 4$. Equivalently, every map in the sense of Definition 2.1 can be colored with four colors.

Remark 5.2（On the proof of this theorem）

The proof was given by Appel and Haken (1976, including the computational part carried out with Koch’s collaboration) and substantially simplified in 1997 by Robertson, Sanders, Seymour and Thomas. Both proofs involve checking finitely many cases by computer and are far too long for this article. In §5.1 below and in §6 we describe the skeleton of the proof and its character. For the complete argument see Robertson–Sanders–Seymour–Thomas (1997) in the references, and for the formalization see Gonthier (2008).

5.1. The skeleton of the proof

The framework of the proof has not changed since the nineteenth century. Take a minimal counterexample and show that it cannot exist.

flowchart TD
A["Suppose the four color theorem is false"] --> B["Take a counterexample G with fewest vertices"]
B --> C["Unavoidability: G must contain at least one<br/>of the configurations on our list"]
B --> D["Reducibility: for no configuration on the list<br/>can a minimal counterexample contain it"]
C --> E["Contradiction"]
D --> E
E --> F["No minimal counterexample exists<br/>= the four color theorem is true"]

The skeleton of the proof of the four color theorem. All the difficulty is pushed into the two boxes marked unavoidability and reducibility, and their contents become the computer's work.

Definition 5.3（Configurations, unavoidable sets, reducible configurations）

A configuration is a part of a planar graph: several vertices together with a small subdiagram carrying the information of their degrees.

A finite set $\mathcal{U}$ of configurations is an unavoidable set if there is no planar triangulation containing none of the configurations in $\mathcal{U}$. In other words, every map is bound to contain somewhere at least one of the shapes in $\mathcal{U}$.

A configuration $K$ is reducible if, for a planar graph $G$ containing $K$, one can show that $G$ itself has a 4-coloring under the assumption that all planar graphs smaller than $G$ have one. In short, $K$ cannot occur inside a minimal counterexample.

If every member of an unavoidable set is reducible, then a minimal counterexample must both contain and fail to contain one of these shapes, a contradiction. That finishes the proof.

Corollary 3.4 is the most primitive instance of this framework. The five configurations “a vertex of degree at most 5” form an unavoidable set. And what the proof of the six-color theorem showed is that in a world of six colors all five of them are reducible. For the five-color theorem, Kempe chains were required to prove the reducibility of the degree-5 configuration. With four colors, these five configurations fall hopelessly short.

5.2. Discharging

The tool for constructing unavoidable sets is discharging, systematized in 1969 by Heinrich Heesch. The principle is elementary.

Give each vertex $v$ the initial charge $6 - \deg(v)$. In a triangulated planar graph $E = 3V - 6$ holds (the case of equality in Lemma 3.3), so the total charge is

$$\sum_{v} \bigl(6 - \deg(v)\bigr) = 6V - 2E = 6V - 2(3V-6) = 12 .$$

However many tens of thousands of vertices there are, the total charge is always 12. In particular a vertex of positive charge, that is a vertex of degree at most 5, must exist. This is another proof of Corollary 3.4.

Now the discharging method proper begins. One designs rules of the form “move charge, according to prescribed rules, from vertices of positive charge to nearby vertices of negative charge”. Moving charge does not change the total of 12, so after the moves some positive charge still remains somewhere. If the rules are well designed, one obtains the conclusion that for positive charge to remain at a vertex after the moves, the surroundings of that vertex must have a particular shape. Collecting all these particular shapes gives an unavoidable set.

In the proof of Robertson and his coauthors, 32 discharging rules produce an unavoidable set of 633 configurations. Each of these 633 is then checked for reducibility by computer. Testing the reducibility of one configuration is a finite computation: try every coloring of its boundary and see, by repeated Kempe chain interchanges, whether it extends to the interior. What is being done is the same “counting of cases” as in tabulating and counting every case（Example 3.3）［The Monty Hall Problem］, and although finite, it involves thousands to tens of thousands of cases per configuration, which makes hand computation unrealistic.

Tip

In Appel and Haken’s 1976 proof the unavoidable set consisted of 1936 configurations (later reduced to 1482), and the computation took about 1200 hours on an IBM 370-168. The reduction to 633 in the 1997 version came from redesigning the discharging rules so as to select only configurations whose reducibility is easy to check. The effort to shorten a proof continues after the theorem has been established.

6. Can a proof written by a computer be believed?

In June 1976 the University of Illinois began using a postmark reading “Four colors suffice”. Such celebrations are rare in the history of mathematics, but the reaction of the mathematical community was not uniform.

The objection went as follows. A proof ought to be something that, in principle, a single mathematician can read and be convinced by. Can an argument that nobody can read in its entirety be called a proof?

At least three distinct issues are mixed together in this criticism. Separating them clarifies matters.

Issue	Content	Present status
Verifiability	If nobody can check the whole thing, how is correctness guaranteed?	The 1997 version was independently reimplemented, and in 2005 it was formalized in Coq
Possibility of error	Bugs in the program, defects in the compiler, hardware failure	Formalization has all but eliminated error in the argument; trust in the implementation remains
Understanding	We still do not know why it is 4	Almost untouched. This remains an open question today

The first issue has largely been resolved. The programs of the 1997 proof of Robertson and his coauthors were published and have been reproduced by several independent implementations. Moreover, in 2005 Georges Gonthier used the proof assistant Coq to formalize the whole of the four color theorem. Both the discharging argument and the reducibility checks were rewritten in a form verifiable by Coq’s small logical kernel. What the reader must trust is no longer “Appel and Haken’s Fortran program” but “the correct implementation of Coq’s kernel”. The kernel is a few thousand lines long, and many people have read it.

The second issue has weakened considerably for the same reason. It has not vanished, though. There is no guarantee that Coq’s kernel is free of bugs, nor that computers do not fail. But one may equally say that this differs only in degree from the possibility that a long proof written by a human contains an error. Kempe’s “proof”, after all, passed human refereeing for eleven years.

Only the third issue remains. Following the proof of the four color theorem to the end does not tell us why four rather than five suffices. All one can say is that all 633 cases happened to be reducible. A mathematical proof has two functions: guaranteeing correctness, and explaining the reason. The proof of the four color theorem performs the first and hardly performs the second at all. That mathematics is hard not because of its many symbols but because of the existence of this sort of “understanding that does not feel like understanding” is discussed in Why mathematics is hard as well, there from the side of what a proof is（Definition 4.1）［Why Mathematics Is Hard］.

Example 6.1（On a doughnut, seven colors are needed）

The four color theorem is a phenomenon peculiar to the plane (and the sphere). Drawing maps on the surface of a doughnut (a torus) changes the situation.

On the torus one can draw $K_7$, the graph on seven vertices in which every two are joined, without crossings. Hence a map of seven mutually adjacent countries exists there, and seven colors are needed. Conversely, seven colors can be proved sufficient. On the torus Euler’s formula becomes $V - E + F = 0$, so redoing the same computation gives $E \le 3V$, whence the existence of a vertex of degree at most 6. From there the same induction as for the six-color theorem reaches seven colors.

What is striking is that this proof of “7” is far easier than the four color theorem. In 1890 Heawood conjectured that for a surface of genus $g \ge 1$ the necessary and sufficient number of colors is

$$\left\lfloor \frac{7 + \sqrt{1 + 48g}}{2} \right\rfloor$$

(substituting $g=1$ gives $\lfloor (7+7)/2 \rfloor = 7$). The conjecture was proved in 1968 by Ringel and Youngs. So all the surfaces with holes had been settled, and only the plane, which looks the simplest of all, held out to the end.

7. Exercises

Exercise 7.1Easy

Show, using Lemma 3.3, that the graph $K_5$ on five vertices in which every two are joined is not planar.

Solution

$K_5$ has $V = 5$ vertices, and its number of edges is the number of ways of choosing 2 objects from 5, that is $E = \binom{5}{2} = 10$.

Suppose $K_5$ were planar. It is simple and has $V = 5 \ge 3$, so Lemma 3.3 applies and gives

$$E \le 3V - 6 = 3 \cdot 5 - 6 = 9 .$$

But in fact $E = 10 > 9$. This contradiction shows that $K_5$ is not planar.

Note that, as we saw in Example 2.3, $K_4$ can be drawn in the plane ($V=4$, $E=6 \le 3\cdot4-6 = 6$, just barely). The largest number of countries that can be pairwise adjacent in the plane is 4, and this is the reason four colors are necessary. Observe, however, that “four colors suffice” does not follow from this. There are plenty of graphs which contain no $K_5$ and yet require four colors.

Exercise 7.2Standard

Let $G$ be a connected simple planar graph with $V \ge 3$ vertices, and suppose in addition that $G$ contains no triangle (no cycle of length 3). Show that $E \le 2V - 4$, and use this to show that $K_{3,3}$ — the graph obtained by joining every vertex of one group of three to every vertex of another group of three — is not planar.

Solution

First part. We follow the proof of Lemma 3.3. Fix a plane drawing of $G$ and let $F$ be the number of faces. Since $G$ contains no triangle, every boundary walk has length at least 4. Indeed, a boundary walk of length 3 would require a cycle of length 3, which the hypothesis excludes (that lengths 1 and 2 are excluded by simplicity and by connectedness with $V \ge 3$ is exactly as in that proof).

Every edge occurs exactly twice among the boundary walks, so

$$2E \ge 4F, \qquad \text{that is} \quad F \le \tfrac{1}{2}E .$$

By Proposition 3.1 we have $F = 2 - V + E$, hence

$$2 - V + E \le \tfrac{1}{2}E .$$

Subtracting $\frac{1}{2}E$ from both sides gives $2 - V + \frac{1}{2}E \le 0$, and rearranging yields $E \le 2V - 4$.

Second part. $K_{3,3}$ has $V = 6$ vertices and $E = 3 \times 3 = 9$ edges. Being bipartite, it has no cycle of odd length and in particular no triangle (every edge crosses between the two groups, so every cycle has even length). It is also connected.

If $K_{3,3}$ were planar, the inequality of the first part would apply and give

$$E \le 2V - 4 = 2 \cdot 6 - 4 = 8 ,$$

whereas in fact $E = 9 > 8$. The contradiction shows that $K_{3,3}$ is not planar.

(Since $K_{3,3}$ satisfies $E = 9 \le 3V-6 = 12$, non-planarity does not follow from Lemma 3.3 alone. The extra information that there is no triangle was needed.)

Exercise 7.3Standard

Draw finitely many straight lines in the plane, dividing it into regions. Show that the map so obtained can always be colored with two colors.

Solution

Let the lines be $\ell_1, \ldots, \ell_n$. Each line $\ell_i$ divides the plane into two open half-planes, so for each region $R$ we obtain a value

$$s_i(R) = \begin{cases} 0 & (R \text{ lies on one side of } \ell_i) \\ 1 & (R \text{ lies on the other side}) \end{cases}$$

Since a region is a connected set not crossing any line, $s_i(R)$ is uniquely determined by $R$. Now set

$$c(R) = s_1(R) + s_2(R) + \cdots + s_n(R) \bmod 2$$

and take $c(R) \in \{0, 1\}$ as the color.

Suppose two regions $R, R'$ are adjacent. Their common border is a segment (or a ray), and it is part of exactly one line $\ell_k$. Crossing this border from $R$ to $R'$ switches only the side with respect to $\ell_k$, leaving the side with respect to each other $\ell_i$ ($i \ne k$) unchanged, because one can pass through an interior point of the border without crossing any other line (an interior point of the border may be chosen so as to lie on no line other than $\ell_k$).

Hence $s_k(R') = 1 - s_k(R)$ and $s_i(R') = s_i(R)$ for $i \ne k$, so that

$$c(R') = c(R) + 1 \bmod 2 \ne c(R) .$$

Therefore $c$ is a 2-coloring, and a subdivision by straight lines can always be colored with two colors.

(The same argument works for subdivisions by circles. The idea that crossing an odd number of times changes the color is one instance of the technique of constructing an invariant and comparing, just as in the digit-shifting argument（Proposition 3.4）［Is 1 Equal to 0.999…? Fixing the Meaning of an Infinite Decimal First］ used to verify $1 = 0.999\ldots$.)

Exercise 7.4Hard

Explain, stage by stage in the proof of Theorem 4.3, what stops working when the number of colors is reduced from 5 to 4. State also why the “two interchanges” that Kempe needed in handling a vertex of degree 5 are dangerous.

Solution

(1) The guarantee that a color is left over disappears. In the five-color proof we finished immediately when $\deg(v) \le 4$, or when the neighbors used at most 4 colors. All that remained was the case ”$\deg(v) = 5$ and the neighbors use all five colors”. With four colors, both the case $\deg(v) = 4$ with the neighbors using all four colors and the case $\deg(v) = 5$ remain. The former is handled by a single Kempe chain interchange exactly as with five colors (if $v_1$ and $v_3$ are not joined by a $(1,3)$-Kempe chain, interchange to free color 1; if they are, the same planarity argument as in Theorem 4.3 shows that $v_2$ and $v_4$ are not joined by a $(2,4)$-Kempe chain). The trouble is with the latter.

(2) At degree 5 the neighbors necessarily repeat a color. If $\deg(v) = 5$ and only four colors are available, the colors of the neighbors $v_1,\ldots,v_5$ must repeat somewhere. Because of the repetition, a free color does not come out automatically, and a fine case analysis according to the arrangement of colors is required. In one branch of the analysis one is required, for example, to interchange along a $(1,3)$-Kempe chain and then along a $(1,4)$-Kempe chain in succession.

(3) Why two interchanges are dangerous. The definition of a Kempe chain (Definition 4.1) depends on the coloring $c$ in force at that moment. Performing the first interchange changes the coloring from $c$ to $c'$, so the Kempe chains with respect to $c$ and those with respect to $c'$ are in general different objects. Concretely, interchanging colors 1 and 3 first turns vertices previously colored 3 into vertices colored 1, so new vertices may join the $(1,4)$-Kempe chains and connected components may merge. If they merge, the premise of the second step — ”$v_1$ and $v_4$ lie in different components, so we may interchange” — collapses.

Kempe overlooked this dependence. In 1890 Heawood constructed a map with 25 countries in which exactly such a merging occurs, showing that Kempe’s argument does not close. That the proof of Theorem 4.3 manages with a single interchange is thanks to the slack afforded by one extra color.

(4) Hence one enlarges the configurations. The modern proof avoids this difficulty by dealing not with “configurations around one vertex”, such as the neighborhood of $v$, but with large configurations spanning dozens of vertices. The 633 configurations mentioned in §5 are, in this sense, a redecomposition into finitely many large chunks of the place where Kempe failed at a single vertex.

References

• Robin Wilson, Four Colours Suffice: How the Map Problem Was Solved, Allen Lane, 2002 (Japanese translation: Yonshoku Mondai, translated by Kenichiro Mogi, Shinchosha, 2013) — a general-audience history of the four color problem. For the story from Guthrie to Appel and Haken this book is the fullest and the most readable.
• Shin Hitotsumatsu, Yonshoku Mondai: Sono Kaiketsu to Tenkai, Kodansha Blue Backs, 1978 (in Japanese) — an exposition written just after the Appel–Haken proof; it follows discharging and reducibility with formulas.
• N. Robertson, D. Sanders, P. Seymour, R. Thomas, “The four-colour theorem”, Journal of Combinatorial Theory, Series B 70 (1997), 2–44 — the proof now regarded as standard, built from 633 configurations and 32 discharging rules.
• G. Gonthier, “Formal Proof — The Four-Color Theorem”, Notices of the American Mathematical Society 55 (2008), 1382–1393 — the report on the complete formalization in the proof assistant Coq. PDF
• R. Diestel, Graph Theory, 5th ed., Springer, 2017 — Chapter 5, Colouring, contains the proof of the five-color theorem and an outline of the proof of the four color theorem. Euler’s formula is in Chapter 4.
• J. A. Bondy, U. S. R. Murty, Graph Theory, Springer GTM 244, 2008 — a standard textbook on planar graphs and coloring, including an introductory account of discharging.

Appendix: Equivalent reformulations of the four color theorem

The four color theorem as an edge coloring. In 1880 Peter Guthrie Tait translated the four color problem into a problem about coloring edges. Consider the situation in which the borders of a map always meet three at a time — that is, a planar graph every vertex of which has degree 3, a cubic planar graph. Then the following holds: for a cubic planar graph with no bridge (an edge whose removal increases the number of connected components), the faces can be 4-colored if and only if the edges can be colored with three colors so that edges meeting at a vertex receive different colors.

The device behind the translation is to regard the four colors as the elements $\{0, a, b, c\}$ of the Klein four-group. Defining the color of each edge to be the sum, in the group, of the colors of the two faces on its sides, one recovers a 3-coloring of the edges from a 4-coloring of the faces, and conversely a 4-coloring of the faces from a 3-coloring of the edges.

Tait’s failure. Tait went on to assume that every cubic planar graph without a bridge has a Hamiltonian cycle (a cycle passing through every vertex exactly once). Given a Hamiltonian cycle a 3-coloring of the edges is easy to produce, so the four color theorem should have followed. But the assumption is false. In 1946 W. T. Tutte constructed a counterexample on 46 vertices. Kempe’s error was found after eleven years; Tait’s survived for sixty-six (the location of the error itself had been pointed out by Julius Petersen in 1891).

The moral. The four color problem has repeatedly displayed the property of becoming vastly easier once one plausible-looking lemma is inserted — and every one of those lemmas turned out to be false. That a counterexample can appear after dozens of confirmations is the same moral as the formula that works 40 times and fails on the 41st（Example 4.2）［Why Mathematics Is Hard］. For the record of famous mathematicians who slipped on this problem, read Famous mathematicians as well. The history of proof is the history of correct theorems and, at the same time, the history of plausible errors.