The Four-Color Theorem Gets a Rare New Proof
The four-color theorem is simple to state: Given a contiguous map, is it possible to color each region with one of four colors such that no neighboring regions share a color?
Vico Santos for Quanta Magazine
Introduction
Some math problems continue to haunt researchers long after they’ve been solved. A proof emerges, is even celebrated, and yet dissatisfaction lingers. Perhaps the argument is too convoluted — the hunt persists for the elusive one-page paper — or perhaps it fails to give a deeper theoretical insight into why something is true. Whatever the reason, mathematicians return, again and again, to a case that is otherwise considered closed.
One of the most famous such cases is that of the four-color theorem, a problem that transformed how mathematicians think about their subject.
The problem is simple to state, and even simpler to see: Given a contiguous map, is it possible to color each region with one of four colors such that no neighboring regions share a color? In the mid-19th century, the question was of trifling interest to mapmakers, who had far more than four colors at their disposal and saw no particular reason to restrict their palette. But to mathematicians, both amateur and professional, the brain teaser quickly turned into an obsession.
The first purported proof, announced in 1879, stood for 11 years before it was proved incorrect. More wrong answers would follow, from lawyers and doctors and famous graph theorists, too. “Here we have a problem that even a child can understand,” said Carsten Thomassen, a graph theorist at the Technical University of Denmark. “I think that’s the reason why it has been such a big challenge.”
The theorem was finally proved nearly a century later — but with computer methods that were considered scandalous at the time, causing mathematicians to question what they considered a proof in the first place. The status of the problem remained a source of debate until 1997, when the use of computers became more common and a simpler computer-assisted proof was found.
Yet even today, the “four-color disease,” as Mikkel Thorup, a computer scientist at the University of Copenhagen, puts it, continues to circulate. He and Thomassen count themselves among the afflicted. For such a simple statement, there must be a simpler reason why it is true. Or at least a more efficient way to demonstrate it.
After nearly a decade of work, Thorup, Thomassen, and four colleagues in Denmark, Canada, and Japan have produced yet another computer proof of the theorem.
From left: Carsten Thomassen, Ken-ichi Kawarabayashi, Mikkel Thorup, and Bojan Mohar are part of a team that recently re-proved the four-color theorem, revealing in the process a more efficient way to color maps and graphs.
Courtesy of Mikkel Thorup
The proof — which was posted online in March 2026 and will be presented in November at the annual Foundations of Computer Science conference — is in some ways even more complicated than its predecessors. “It looks like they’ve used electricity liberally in actually carrying out their proof,” said Georges Gonthier, a computer scientist at Inria in Paris. But in the process of crafting their argument, the researchers provided a far more efficient way to color maps. And in doing so, they uncovered new insights into structural properties of important mathematical objects called planar graphs — opening up the potential for progress on many other stubborn problems in graph theory.
Given the problem’s history of false starts and dashed hopes, Gonthier said, “it’s really cool to see a real result for once.”
Computerized Controversy
In 1852, the mathematician Francis Guthrie was coloring in a map of English counties when he noticed that he needed only four colors. Was this always true, he wondered? He asked his brother Frederick, also a mathematician, whose adviser, Augustus De Morgan, took an interest in the question and decided to market it to a wider audience. In 1879, when a mathematician named Alfred Bray Kempe claimed to have a solution, a press release announced the achievement in Nature.
Kempe started by assuming the opposite of what he wanted to prove: that there is a map that can’t be colored with only four colors. He then sought to show that this assumption would ultimately lead to a contradiction — meaning that no such map could exist. In that case, all maps would have to be four-colorable.
First, he said, imagine that the non-four-colorable map from your assumption is as “minimal” as possible: If you were to remove any country from it, the remaining map would be four-colorable. Next, do away with geography and other extraneous details by redrawing your map as what’s known as a planar graph. Represent each country as a point (or vertex), and draw a line (or edge) between two points if those countries share a border. Your map-coloring problem is now a graph-coloring one, opening it up to the tools of graph theory.
Mark Belan/Quanta Magazine
In particular, in the 18th century, the Swiss mathematician Leonhard Euler discovered that planar graphs have many useful properties — among them a guarantee that any such graph will contain at least one vertex with five or fewer neighbors. That means that your graph must have at least one of these six configurations, what Kempe called an unavoidable set:
And because your graph is minimal, if you remove any of these configurations from it, you’ll be left with a graph that can be recolored with four colors. Kempe’s genius move was to show that no matter which of these configurations you remove, you can always find a way to swap the graph’s colors around so that when you add your missing vertex back, it’s possible to color all the vertices without needing a fifth color.
Mark Belan/QuantaMagazine
By showing that each unavoidable configuration is “reducible” in this way, you’ve demonstrated that your minimal graph is four-colorable after all — your original assumption was wrong. The four-color theorem must be true.
Unfortunately, 11 years after Kempe announced his proof, the mathematician Percy John Heawood discovered a subtle flaw in his color-swapping procedure: In the case where the vertex you remove has five neighbors, Kempe’s method could lead to the same colors ending up next to one another. Heawood was initially reluctant to report the error, in part because Kempe’s approach was so elegant. And indeed, despite Kempe’s error, his swapping procedure — today known as a Kempe chain — would remain at the core of future solutions to the problem. “Isn’t it interesting that you make a mistake which is so interesting that it’s named after you?” Thomassen said.
In the end, no one was able to show that the last configuration in Kempe’s unavoidable set was reducible. It turned out that a correct proof would instead require identifying a much larger, more complicated set of 8,900 configurations — and showing that all of them are reducible. The task was impossible to deal with by hand. It needed computers.
In 1976, the mathematicians Kenneth Appel and Wolfgang Haken figured out a clever way to lower the number of possibilities first to 1,936 configurations, and then to 1,482. They then used the supercomputers at the University of Illinois to properly reduce each one. At last, they said, the four-color theorem was settled.
The British mathematician Augustus De Morgan sought to stir up broader interest in the four-color problem. “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,” he wrote in an 1852 letter to the prolific mathematician and physicist William Hamilton.
Public Domain
They met a skeptical audience. Computers at the time were scary, technically unknowable. Appel and Haken were using core memory, storing information on magnetic material that was hand-woven into a mesh of wires. “There were all kinds of arguments about how you can possibly trust this proof,” said Ellen Gethner, a mathematician at the University of Colorado, Denver. “What happens if there’s a surge of electricity and you miss that one configuration that would have invalidated the proof?”
Still, most people grew to eventually accept that “four colors suffice,” as the University of Illinois later announced on their postal meter stamps. And in 1997, a team of mathematicians put the matter to bed by simplifying Appel and Haken’s approach, using a computer to identify and check just 633 configurations. This time, the mathematical community accepted the result immediately.
But the story was far from over.
Searching No-Man’s Land
The latest chapter started on a Danish beach in 2015.
Ken-ichi Kawarabayashi, a graph theorist at Japan’s National Institute of Informatics, was at a conference with Thorup, his longtime collaborator. The pair had recently published a major paper together (which would later win them the prestigious Fulkerson Prize, also awarded decades earlier to Appel and Haken for their four-color work). They now stood on the white sand of Nyborg, wondering what to do next. “We can’t really work on a small project,” Kawarabayashi recalled thinking.
The four-color theorem had been a huge influence throughout their careers. It had inspired them, in part, to become graph theorists in the first place. Yet they remained dissatisfied with one aspect of the 1997 result: It had given mathematicians a recipe for coloring any graph with four colors, but that recipe was inefficient. For a graph with n vertices, the coloring process would require n2 steps.
The problem was that if you were handed some large graph and wanted to color it, you would have to search through it for one configuration, remove it, then search for another configuration, remove that, and so on — until you’d reduced your graph to something that was clearly four-colorable.
Kawarabayashi and Thorup, soon joined by Thomassen and Bojan Mohar of Simon Fraser University, wanted to identify an unavoidable set of configurations that could be reduced in parallel, rather than one by one. To do so, they’d have to guarantee that they could reduce each configuration without interfering with the colorings of the other configurations getting reduced at the same time. That would give them a far faster way to recolor a graph with just four colors.
How to find these non-interfering configurations? By searching widely.
In the 1976 and 1997 proofs of the four-color theorem, mathematicians focused only on regions that featured clusters of vertices with few connections. Kawarabayashi, Mohar, Thomassen, and Thorup instead directed their attention to so-called flat areas of the graph, where every vertex is connected to six others, forming a triangular arrangement of edges. These areas form a sort of graphical no-man’s land: It’s harder to identify good configurations there, since flat regions lack the structure that’s usually used to prove a configuration’s reducibility. But, the researchers figured, flat areas are also much more common. And to reduce and recolor many configurations at once without letting them interfere with each other, they’d need a lot of options to choose from.
Atsuyuki Miyashita (left) and Yuta Inoue helped search for important structures in regions of graphs that usually get ignored.
Courtesy of Yuta Inoue
The search for configurations in these regions would take two more minds — Kawarabayashi’s graduate students, Yuta Inoue and Atsuyuki Miyashita — and months of computing time. “We were pretty naïve,” Thorup said. “I don’t think we had any clue it would take so long.” But eventually they landed on a new unavoidable set. It was massive, consisting of 8,202 configurations. But as they’d hoped, it was possible to reduce many of those configurations at the same time in a given graph, turning what had once been many steps into just a few.
Once again, the four-color theorem had been proved. And the new proof gave a far more efficient coloring algorithm: For a graph with n vertices, it required n(log n) steps, a significant improvement over n2.
New Horizons
As with Kempe’s failed attempt more than a century ago, the greatest value of the new proof lies less with its headline result than with the new insights it provides into the nature of graphs. By drawing on a different concept of reducibility and using overlooked parts of the graph, the work has revealed previously unknown structure in these important mathematical objects — and has given mathematicians new tools for understanding them. “Once you build up machinery, you find out what kind of problems you can solve,” Gethner said.
For instance, graph theorists are interested not just in planar graphs, but in graphs that lie on all sorts of surfaces, such as the doughnut-shaped torus. These graphs have some of the same properties that the new work uncovered in planar graphs — making it possible to prove coloring theorems about them as well. The researchers behind the latest four-color result are now using their techniques to address these questions. Though obstacles remain, Thomassen said, “I think we have the right path.”
Meanwhile, the four-color disease lives on. While Thomassen is pleased with his recent result, he still has the same question that has dogged hobbyists and professionals alike for 150 years: Is there a simpler explanation for why four colors suffice for any planar graph? The mythical one-pager, the theoretical flourish that would make everyone go “aha”?
“What I would like is a proof without the use of a computer,” Thomassen said. “And I will never stop thinking about that.”
