Four color theorem

The great mathematician, Herman Minkowski, once told his students that the 4-Color Conjecture had not been settled because only third-rate mathematicians had concerned themselves with it. "I believe I can prove it," he declared. After a long period, he admitted, "Heaven is angered by my arrogance; my proof is also defective."
(The Four Color Problem: Assaults and Conquest. Saaty & Kainen, 1986, p.8)

Ever notice that most maps aren't really that colorful? Your average, run-of-the-mill map usually only has four colors. If you just start coming up with fake maps, you can always find a way to color the whole thing with four colors, and two adjacent countries will never have the same color.

Way the heck back in 1856, a few mathematically-inclined brothers noticed this. They couldn't prove it, so they brought it to a teacher of theirs, the storied professor Augustus De Morgan. Morgan could not prove this conjecture. Word of this odd problem slowly spread, until it was presented to the London Mathematical Society in 1878, and the problem was then published. One by one, mathematicians attacked the problem, only to fall short. Not that their effort was wasted; Kempe chains were first formulated to try and solve this problem, and a man named John Tait solved a similar problem based on three colors.

In 1976, two men named Kenneth Appel and Wolfgang Haken came up with a solution. This solution involved breaking up the problem into about 1500 smaller problems, and then programming a computer to directly prove all of these cases. In other words, Appel and Haken made a computer check each and every single case they could think of. It took 1200 hours of processing to finish, and they triumphantly published their work - solving a problem that has lasted over 100 years.

This, however, brought up another problem. Mathematicians just won't trust you when you say that you've solved a problem. No, they gotta check the work. By hand. But how do you check the work of a computer? If a computer had to do the work in the first place, how can a human go through and make sure that everything the computer did was right? After a few tries, most mathematicians just accepted that they were probably right. This is the only proof in existence that people believe is solved without anyone actually checking all the work by hand.

A two-dimensional geographic map may be colored with four colors such that no two regions adjacent to one another share the same color.

That's it in laymens' terms. I should note that adjacency means more than just a point, since, obviously, you could have arbitrarily many regions adjacent at exactly one point, and thus no n-color theorem could be true for any n.

This is a result of the field of graph theory, a branch of mathematics/combinatorics/computer science. This theorem was first proved in 1976, though it had been postulated at least ninety years earlier.

I'll leave it to others to post the graph-theoretic theorem.

A slightly more rigorous definition: The faces of any planar graph can be labeled with at most 4 "colors" such that no two adjacent faces have the same label.

The proof Soft Picasso alluded to involved breaking the problem into over 1000 test cases and checking each by computer. As such, there was very little theoretical mathematics involved, so nobody really knows why it's true.

The equivalent 6-color theorem can be easily proved using elementary graph theory. The proof of the 5-color theorem is more difficult but still understandable to a first-semester student of graph theory. Once again, there simply is not a known satisfactory theoretical proof of the 4-color theorem.

It's interesting to note that the theorem that any map requires four colors to color it only applies to planar and spherical maps. For instance, a map drawn on a torus may require seven colors, but never more than that; a map drawn on a double torus requires no more than eight. Proving these unusual topological cases was actually done long before the four color theorem could be proved.

See also the four-color theorem

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.

I think jes5199 and I have observed the same phenomenon : by starting from a 3-country map and adding countries one by one in such a way that they touch as many already-added countries as possible, you'll always be able to colour the new country. The problem is: not every planar graph can be constructed in this way! Simple counterexamples are a dodecahedron and a Rubik's cube (which are planar topologically).

So if I ever had some time to spare on it, what I'd try is finding a set of construction operators for colored graphs that only add or substitute subgraphs, preserve colours, and can produce every planar graph.

See also the two color theorem.