# Intuition behind the “large but finite search space” of the proof of the four colour theorem?

I know the four colour theorem was solved by a computer checking a large number of cases. What I don't understand is why there are only a large but finite number of cases. It seems like there should be infinitely many planar graphs... What is the intuition behind cutting this down to a finite number of configurations?

-
The question in the title and the question in the body are different: one askes for the intuition about the theorem and the other for the intuition about the (current) proofs. People are answering the body... (I would love an intuitive explanation for the theorem itself, though!) – Mariano Suárez-Alvarez Sep 14 '10 at 15:26
I think the wikipedia article I linked to does an adequate job of explaining the content of the theorem. – Seamus Sep 15 '10 at 10:40
sure but I meant, an intuitive explanation of why one would expect the theorem to be true, not of what the statement means. – Mariano Suárez-Alvarez Sep 15 '10 at 11:45
In the comments to my answer, Seamus clarifies that he gets how the proof works and would like a heuristic argument as to why there should be a finite unavoidable set of reducible configurations. I don't know. Any ideas? – David Speyer Sep 15 '10 at 14:11

I'm not sure whether or not you understand how the proof of the $4$ color map theorem worked. I'll sketch that, and then make some philosophical comments.

Let's start by proving the $6$ color map theorem. Without loss of generality, we may assume that all the faces of our graph are triangular, because adding edges just makes a graph harder to color. (We are coloring vertices.) Let $V$, $E$ and $F$ be the number of vertices, edges and faces. Every edge is in two faces, and every face has three edges, so $F=(2/3)E$. We have $V-E+F=2$ by Euler's relation, so $V=E/3 +2$. Since the sum of all vertex degrees is $2E$, the average degree of a vertex is $2E/V = (2E)/(E/3 + 2) < 6$. So the average degree is less than $6$ and there must be a vertex $v$ of degree $\leq 5$. Delete $v$, $6$-color the rest of the graph (by induction), and add $v$ back. Since the vertex has degree $\leq 5$, there is some color which does not border $v$, color $v$ that color.

To prove the $5$ color map theorem requires one new idea. Find the vertex $v$ as before, color the rest of the graph and add it back. But we have a problem if the $v$ has degree $5$ and its neighbors all have different colors. The idea to get around this is to consider the subgraphs $G_{ij}$ consisting of vertices of colors $i$ and $j$, for different pairs $(i,j)$. Because $G_{ij}$ and $G_{k \ell}$ can not cross, for $i$, $j$, $k$ and $\ell$ distinct, some of these graphs must be disconnected. By considering the finitely possible many arrangements of these graphs, one sees that, in each case, one can take some component of $G_{ij}$ and switch the colors $i$ and $j$ on that component in order to make $v$ have only $4$ distinct colors of neighbor. See, for example, Wikipedia for details.

The $4$ color map theorem requires the recoloring idea of the previous paragraph, plus one more idea. Instead of showing that there is always a vertex of degree $3$, $4$ or $5$, one shows that one of a finite list of larger configurations is unavoidable. This list tends to have 600-2000 members, depending on exactly which copy of the proof you read. The idea to showing that this list is unavoidable is an averaging argument like the one I used; the technical term to search for is "discharging". For each of these hundreds of configurations, one removes it from the graph, colors the rest, and analyzes the possible positions of the graphs $G_{ij}$. In each case one can recolor some of the components of the $G_{ij}$ in such a way that, when the configuration is put back in, the whole graph will be colorable.

As I understand it, computers are used in two ways. The less interesting one is that there is a routine which verifies that the discharging argument is correct, finds the possible positions of the $G_{ij}$ and checks that they can be recolored.

The more interesting one is that, when the routine in the previous paragraph fails, the computer perturbs the discharging argument, finds a new resulting list of configurations and tries again. It is basically a genetic process, where the computer tweaks the discharging algorithm until it finds a list of configurations which works.

The leap of faith which Appel and Haken took was to believe that there was some sufficiently complex discharging algorithm, and some list of configurations for which this procedure would work, and they just had to search long enough. Since then, this search has been implemented many times, with the details of the search algorithm different in each case, and many different solutions have been found.

To my mind, the whole thing reminds me of parallel evolution. There are lots of ways to make a wing, and if you leave an organism for long enough in an environment that rewards flight then it will develop one. But all of those ways are so complex that a human intellegence couldn't engineer them. Similarly, there are lots of discharging algorithms that prove the $4$ color map theorem, but they are all too bizarre for a human mathematician to find directly.

-
"There are lots of ways to make a wing, and if you leave an organism for long enough in an environment that rewards flight then it will develop one." Is that a theorem of evolutionary biology? If so, I'd like to see the proof. (More plainly, I think you are probably exaggerating a bit for dramatic effect, n'est-ce pas?) – Pete L. Clark Sep 14 '10 at 22:05
Yup, I am exaggerating. Also, engineers have been known to design wings. But this really is the vague intuition I have for why these searches work. – David Speyer Sep 14 '10 at 23:00
The approach above is the usual one for proving the 5-color theorem of Heawood, however, relatively recently there is a new approach which does not require the use of Euler's Polyhedral formula but depends directly on the Jordan Curve Theorem: Thomassen, Carsten (1994), "Every planar graph is 5-choosable", Journal of Combinatorial Theory, Series B 64: 180–181 . – Joseph Malkevitch Sep 15 '10 at 2:18
Nitpicking aside, this is a very nice answer. – Pete L. Clark Sep 15 '10 at 4:05
"one of a finite list of larger configurations is unavoidable. This list tends to have 600-2000 members" This is exactly the point I don't get, the point I wanted an intuitive explanation of. – Seamus Sep 15 '10 at 10:44

Perhaps this expository account of an "improved" proof of the 4-color theorem will help:

-