One of the great episodes in the history of mathematics began on October 23, 1852. In a letter to Sir William Rowan Hamilton, Augustus De Morgan wrote, “A student of mine asked me today to give him a reason for a fact which I did not know was a fact — and do not yet.” To this day, that “fact” continues to enthrall and challenge scholars.

The student was Frederick Guthrie, and the “fact” in question originally came from his brother, Francis. After looking at a map of British counties, he wondered whether it was always possible to color a map using four or fewer colors, while ensuring that regions sharing a border (more than a corner point) are different colors.

It seemed as if this should always be possible. “The more I think of it the more evident it seems,” De Morgan wrote. Still, the problem didn’t excite Hamilton. He replied, “I am not likely to attempt your ‘quaternion of colours’ very soon.” And De Morgan’s efforts to get others interested failed as well.

The problem sat largely dormant until 1878, when Arthur Cayley asked members of the London Mathematical Society if anyone had found a proof. Soon after that, proofs started appearing. It was the first one, by the barrister Alfred Kempe in 1879, that turned out to be the most important. The proof was convincing, and it was accepted as correct for over a decade. Unfortunately, Kempe’s proof — like all the others that would appear for the next century — was flawed. Yet it was ingenious, and it contained key ideas that would appear in the eventual proof.

To understand how Kempe and most mathematicians have looked at this problem, it helps to recognize that a map contains a lot of information irrelevant to the coloring problem, such as the shape, size and exact location of each region. All that matters is which regions share boundaries, although we do require all regions to be connected; Michigan, with its separate upper peninsula, doesn’t actually prevent the U.S. map from being four-colorable, but it could, mathematically.

To focus on the information that matters, we can encode these relationships using a graph, also known as a network, where dots (vertices) are connected by lines (edges). Replace each region of the map with a vertex and connect the vertices of neighboring regions with an edge. If it helps, we can imagine that the vertices are the capital cities and the edges are roads joining them.

In this way, the map coloring problem becomes a graph coloring problem: Color the vertices so neighbors are different colors. The minimum number of colors is called the chromatic number of the graph. We can ask about the chromatic number of any graph, but graphs that come from maps have special properties. These graphs are simple, meaning there are no edges starting and ending at the same vertex (called loops), and two vertices can only be joined by one edge. The graph is also planar, meaning it can be drawn so no edges cross.

We can now restate Francis Guthrie’s problem: Prove that the chromatic number of every simple planar graph is at most four.

Here’s a sketch of Kempe’s argument, described in modern terms using graphs rather than maps. He started by observing that a graph with one vertex — perhaps the map is a lone island — requires only one color. He then used a clever argument to build upward from there, arguing that it’s possible to use at most four colors to color a graph with two vertices, then three vertices and so on. Here’s how.

Suppose we can color all simple planar graphs with n vertices with at most four colors — this is trivial for n less than 5 — and we are then handed one with n + 1 vertices. How can we show that it, too, will be colorable with at most four colors?

First, Kempe showed, using a careful counting argument, that every simple planar graph has something in common: It must contain at least one vertex with at most five neighbors. Taking all the options into account, this means that every possible graph based on a map contains one of six special configurations of vertices.

If we remove this vertex, and all the edges that connect to it, we leave behind a graph with n vertices — which we already know can be colored using four colors. We actually do so as the next step. Now, look at the vertices adjacent to the removed vertex. If they exhibit three or fewer colors, we can color the removed vertex one of the remaining colors, and we’re done: We’ve just shown that the graph with n + 1 vertices can be colored with four colors. And if the adjacent vertices include all four colors, Kempe devised a clever method of recoloring certain vertices to free up a color for the removed vertex, again showing that the graph with n + 1 vertices needs only four colors.

In 1890, the mathematician Percy Heawood identified Kempe’s error. There was a special case in which Kempe’s clever method failed. Heawood remarked that although his own work appeared “destructive [rather] than constructive,” he showed that Kempe’s technique could prove that every map can be colored with five or fewer colors — not quite the original goal, but still impressive.

Heawood also investigated maps drawn on more complicated surfaces. He proved that a map on a doughnut with g holes may need as many as $latex frac{mathrm 1}{mathrm 2} left( 7+sqrt{ 1+48g} right) $ colors (where this value is rounded down to the nearest integer). So decorating an ordinary doughnut may require as many as seven colors of frosting. Yet, in what was becoming a pattern, his proof for general surfaces was incomplete, and we didn’t have a full proof until 1968.

But even when Heawood’s theorem for general surfaces was proved, the four-color problem remained unsolved. Thanks to decades of hard work, though, a proof was in sight.

At a conference in 1976, 124 years after Guthrie posed the problem, Wolfgang Haken announced a proof in collaboration with Kenneth Appel and with assistance from the graduate student John Koch. Reactions were mixed. “I had expected the audience to erupt with a great ovation,” wrote Don Albers, who was present at the talk. “Instead, they responded with polite applause!” It was because rather than producing a pencil-and-paper argument, the team relied heavily on a computer.

They didn’t have a machine directly answer the question, since infinitely many planar graphs are possible, and a computer cannot check them all. However, much as Kempe proved that every graph contains one of six special configurations of vertices, Appel and Haken showed that every graph must have one of 1,936 special configurations. Proving the theorem amounted to showing that we need only four colors to color any graph containing those subgraphs. Breaking down Kempe’s six special cases into 1,936 sub-cases gave them more fine-grained control and made each case easier to check — though the total number was now far too large for a human to verify without assistance. In fact, completing the calculations required over 1,000 hours of computer time.

The mathematical community only grudgingly accepted the results, believing that a proof should be understandable and verifiable entirely by humans. While it was acceptable for computers to perform routine arithmetic, mathematicians were not prepared to cede logical reasoning to a computing device. This conservatism and reluctance to embrace time-saving advancements was not new. In the 17th century, there was similar outcry when some mathematicians used newfangled algebraic techniques to solve problems in geometry. Similar drama may play out again with the rise of machine learning: Will mathematicians accept a theorem discovered and proved by an opaque algorithm?

The proof of the four-color problem was, of course, only the beginning of the computer revolution in mathematics. In 1998 Thomas Hales used a computer to prove the famous conjecture of Johannes Kepler’s that the most efficient way to stack spheres is the one routinely employed to stack oranges in a grocery store. And recently computers helped find “God’s number” — the maximum number of twists required to solve a Rubik’s cube (20 face turns or 26 if half turns count as two.)

Although the four-color problem for maps is settled, many basic questions about graph coloring remain unanswered or are just now being resolved.

Heawood’s work with surfaces showed that we can ask colorability questions about nonplanar graphs. And in fact, the chromatic number of a particular graph does not depend on the surface on which the equivalent map is drawn. For instance, a graph in which every vertex is connected to every other vertex is called a complete graph, and the chromatic number of a complete graph with n vertices is n. So if a large graph contains a complete graph with n vertices, then we know the large graph’s chromatic number is at least n.

This observation does not imply that if the chromatic number of a graph is n, then it contains a complete graph with n vertices. But in 1943, Hugo Hadwiger conjectured something very similar. He believed that if a graph with no loops has chromatic number n, then it has an arrangement of vertices called a $latex K_n$ minor, where deleting some vertices and edges and grouping together others results in a complete graph with n vertices. Rephrased, this conjecture states that if a graph does not have a $latex K_n$ minor, then it can be colored with fewer than n colors. Hadwiger’s conjecture, one of the most important open problems in graph theory, generalizes the four-color theorem, since a planar graph cannot contain a $latex K_5$ minor.

Although graph coloring started with a question in cartography, problems having nothing to do with maps or colors can also fit into the graph-coloring framework. For example, sudoku is a graph-coloring problem in disguise. View each cell as a vertex and the nine digits as the colors. Each vertex has 20 edges coming out of it — one to each cell in its row, in its column and in its 3-by-3 sub-square. This graph of 81 vertices and 810 edges starts with a partial coloring (the given clues). The object of the game is to color the rest of the vertices.

Despite all the attention these coloring problems have received, we still do not have a proof of the original four-color theorem that a human can read. This is not due to lack of trying. Even today, new proofs appear, generate some enthusiasm and, like Kempe’s proof, are shown to contain errors.

The mathematician Paul Erdős used to speak about “The Book” — an imaginary tome containing the most elegant proofs of every theorem. One wonders if The Book contains a human-readable proof of the four-color theorem, and if so, whether we will ever see it.