| | Devlin's Angle |
The story of the Four Color Problem begins in October 1852, when Francis Guthrie, a young mathematics graduate from University College London, was coloring in a map showing the counties of England. As he did so it occurred to him that the maximum number of colors required to color any map seemed likely to be four. The coloring has to meet the obvious requirement that no two regions (countries, counties, or whatever) sharing a length of common boundary should be given the same color.
Guthrie's question became known as the Four Color Problem, and it grew to be the second most famous unsolved problem in mathematics after Fermat's last theorem.
In 1976, two mathematicians at the University of Illinois, Kenneth Appel and Wolfgang Haken, announced that they had solved the problem. But there was a twist. Much of their proof was carried out on a computer, and was far too long for humans to check. Although many mathematicians were initially unhappy that much of the proof was a brute force computation that could not be examined by hand, most accepted the result. But some were less sure. What if the computer program had a hidden flaw that meant it did not behave in exactly the way its developers said it did?
Mathematicians grew more confident in the result when, in 1994, another team produced a different computer proof. Still, there always remained some doubts. With Gonthier's work, which uses a mathematical assistant to check the 1994 proof, those doubts should finally be put to rest.
What makes the new result particularly significant from a reliability point of view is that the proof assistant Gonthiers employed, called Coq, is a widely-used general purpose utility, which can be verified experimentally, unlike the special-purpose programs used in the earlier proofs of the Four Color Theorem. Coq was developed by the French research center INRIA, where Gonthiers was formerly employed, and where much of his work on the Four Color Theorem was done.
Getting one computer to check the work of another in this way amounts to fighting fire with fire. A mathematical assistant is a new kind of computer program that a human mathematician uses in an interactive fashion, with the human providing ideas and proof steps and the computer carrying out the computations and verification. Such systems have been under development over the last thirty years. Other applications include checking the correctness of computer hardware and software.
Since the sizes and shapes of the map regions do not matter, only the way they join together, the Four Color Problem is a question in topology. As we shall see momentarily, it is easily reformulated as a problem about networks (or graphs in the sense that term is used in discrete mathematics), and in fact the network formulation is the one used in most attempts at a solution by professionals, including the eventual successful ones.
After being posed by Guthrie, the four color problem floated around London for over twenty years, being regarded more as a curious brainteaser than a major problem of mathematics. But then, on 13 June 1878, the English mathematician Arthur Cayley asked the assembled members of the London Mathematical Society if they knew of a proof of the conjecture. With this act the real hunt was about to begin.
A year later, one of the members of the London Mathematical Society, a barrister called Alfred Bray Kempe, published a paper in which he claimed to prove the conjecture. But he was mistaken, and eleven years later Percy John Heawood pointed out a significant error in the argument. Heawood was however able to salvage enough to prove that you can color any map with five colors.
Over the years, many professional mathematicians, and an even greater number of Sunday afternoon amateurs, tried to solve the problem, but without success. Like Fermat's last theorem, there are some "obvious" ways to solve the problem that seem, on the face of it, to work, but have subtle errors, and professional mathematicians grew used to receiving claimed proofs from amateurs who would often remain convinced their solution was correct even after the error was pointed out to them.
Here is how to reformulate the Four Color Problem as a question about networks. Within each region of the given map, you place a single point, known as a node of the network. (You can think of these points as the capital cities of the countries, if you wish.) You then join up the nodes to form a network, in much the same way that you might link cities by a rail network. The rule is that two nodes are joined together if, and only if, their respective map regions share a common boundary, in which case the line joining them has to lie entirely within the two regions, crossing over the common boundary. (In terms of a rail link this would mean that the line cannot cross the territory of any third country.) The network this gives shows at a glance the topological structure of the map it represents. Indeed, the problem of coloring the map (in the sense of Guthrie's problem) can be reformulated in terms of coloring the network: color the nodes of the network in such a way that any two nodes which are connected together must have different colors. If all networks can be so colored using four colors, so can all maps, and vice versa.
To prove the (network version of the) Four Color Theorem, you start out by assuming that there is a network that cannot be colored with four colors, and work to deduce a contradiction. If there is such a network, there will be (at least) one that has the fewest number of nodes. That's the one to look at. The idea then is to show that you can find a particular node that can be removed without altering the number of colors needed to color the network. Since that new network has one fewer nodes than the one you started with, and that initial network was chosen to be the smallest that could not be colored with four colors, the new network can be colored with four colors. But then, because of the way you chose the node to remove, that means the original map can be colored with four colors. And there's the contradiction.
So the crux of the proof is to describe the individual processes which are used to reduce a given network to one with fewer nodes without reducing the number of colors necessary to color the network, and to show that any minimal counterexample to the Four Color Conjecture must of necessity contain at least one node that can be so removed. This is the part that turned out to require computer help. Appel and Haken had to identify and examine around 1500 different ways that a node could be appropriately removed and show that any minimal counterexample network must contain at least one node of one of those 1500 kinds.
Appel and Haken started their computer-assisted investigation in 1972 and four years later they had their answer. It took 1200 hours of computer time, during which the computer had to carry out billions of calculations. The two mathematicians themselves had to analyze by hand some 10,000 portions of networks.
With the Appel-Haken result, something had happened that mathematicians had wondered about since computers had first appeared in the 1950s: machines had finally taken over some of the task of proving theorems. With the recent work of Gonthier, it seems that computers have also become indispensable for checking their own proofs! Mathematics will never be the same again.
A final thought to leave you with as we start a new year. To this day it is not known if there can be a short proof of the Four Color Theorem that a human could follow. Most mathematicians think there is not. But who knows?