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?
 A: Perhaps this expository account of an "improved" proof of the 4-color theorem will help:
http://people.math.gatech.edu/~thomas/FC/fourcolor.html 
A: 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.
