Here's a problem Lewis Carroll enjoyed posing to kids like Alice: how many colors do you need to fill in any map so that neighboring countries are always colored differently?

It sounds simple enough. But when a Victorian law student first posed the question, guessing that it could be done with a mere four colors, logician Augustus De Morgan was stumped. While no one could devise a map that required more, a proof that every map requires only four colors proved remarkably elusive. Mapmakers didn't care, but problem-solvers were obsessed for decades, including the Bishop of London, a Kentucky colonel, and a California traffic cop. The question's very intractability has inspired innovations in computing and network theory, but some say it still has no satisfying solution.

Oxford professor Robin Wilson's Four Colors Suffice: How the Map Problem was Solved (Princeton: 2003) presents the colorful history of this conjecture, with an unassuming lucidity that will appeal to the mathematical novice. It's thrilling to see great mathematicians fall for seductively simple proofs, then stumble on equally simple counter-examples. Or swallow their pride: after telling his class that the problem had been wasted on third-rate minds, the great number-theorist Herman Minkowski took weeks at the blackboard trying to solve it, finally admitting, "Heaven is angered by my arrogance; my proof is also defective."

The first dead-end occurred shortly after the problem was first posed in 1852. De Morgan became obsessed with his initial insight that in any group of four regions, each bordering every other, one region must be completely enclosed by the others, and thus safe from forcing any colors outside the group. Though undeniably true, this was a false start: looking at single groups of four, one at a time, fails to take into account the myriad ways these groups might interact in ways that force the use of more colors.

The next failure, which convinced mathematicians worldwide for over a decade, actually took giant steps in the right direction. Cambridge mathematician Arthur Cayley revived the problem in 1878 and suggested a totally new approach: if you assume there exist some maps that need more than four colors, and of those you take only the ones that have as few regions in them as possible, then you'll have a manageable but complete set of counter-examples on your hands. (Wilson calls these the "minimal criminals.") If you can show that none of these counter-examples can possibly exist, then you've shown that four colors suffice. The only problem is, there are lots of them.

London barrister and amateur mathematician Alfred Bray Kempe ran with this approach, devising an elegant method that claimed to cleanly dispatch with all possible counter-examples. He put one region after another at the center of a counter-example-first a two-sided shape, then a triangle, square and pentagon-then ruled them out by listing all the possible chains of regions that could branch off from them. The proof was widely accepted, and Kempe was elected a Fellow of the Royal Society, and even knighted.

But in 1890, Percy Heawood, an Oxford eccentric known for his immense mustache and flowing cape, produced a map that showed that one of Kempe's chains didn't work. Even as he disgraced Kempe, however, Heawood demonstrated the lasting value of his contribution, giving a full Kempe-style proof that five colors suffice. (As a result of Heawood's later work, we now know that any map drawn on a doughnut requires no more than seven colors, not counting sprinkles. "There are, of course, additional reasons why one seldom encounters a map of the United States on one's doughnut," mused novelist Tom Robbins.)

The modern story picks up in 1948, when German geometer Heinrich Heesch realized that if he could find a master set of patterns that can't appear in a minimal criminal, he would rule out all possible counter-examples and have a proof. But finding these patterns was really hard, and there were thousands of them.

Enter the computer. In 1976, after 2000 machine-hours at the University of Illinois, Kenneth Appel and Wolfgang Haken found every single one, turning out the first famous computer-aided proof. Some claimed this was not a proof, since it cannot be verified in detail by a human being. By admitting computer proofs into the canon, writes Robin Wilson, math was "in danger of becoming an empirical science, as fallible as physics." Far from a feat of pure reasoning, the answer appeared to some as a monstrous coincidence.

There's an unwritten law as old as math itself: proof comes with understanding. But Appel and Hanken's proof, while almost certainly valid, doesn't clear anything up. Math is changing because of proofs like theirs: Computer jocks like Stephen Wolfram insist that math needs to get beyond its infatuation with axioms, while string theorists say their results just can't wait for rigorous proof. And strangely, mathematicians are even starting to teach machines to prove theorems on their own. So maybe some day computers will explain why four colors are enough, in terms we can understand.