It seems (and a noder once claimed just that, above) that "just a few cases" need to be examined to prove the theorem. This is almost the inevitable reaction after doodling around for about an hour, trying to come up with a counter-example.

Indeed, "*just a few cases*" are *almost exactly* what Appel and Haken ran on Illiac IV in 1976. While it *does* appear that not many "local" cases are of interest, the problem is that you can connect these local cases in infinitely many ways. Think of it this way: all the tests you did by doodling on paper (no offence meant) just looked at some finite region. But we *know* that the proof must be more complex, because on other two dimensional surfaces (like the torus) the 4 colour theorem is false! Clearly you also have to say something about how the plane (in which you draw your map) limits the ways in which your "simple cases" may interlock. The "4 color property" is a *global* property of the plane, which makes proving the 4 color theorem a matter of examining the *global* case. So we have finitely many "interesting" local configurations, which can be connected up into infinitely many global configurations. To prove the theorem by examination, we need to find a global configuration which is "universal" in the sense of covering all global possibilities.

It turns out that this unlikely program can actually be carried out. Appel and Haken used pencil and paper, and then a computer, to show that indeed only finitely many possibilities need to be taken into account. They then constructed a map which contained all these finite configurations, and coloured in (also on the computer).

Some people are still looking for a "nice" proof.