Rare new proof of the four-color theorem yields faster map coloring and graph insights

The four-color theorem, settled by computer in the 1970s and still a source of quiet dissatisfaction among mathematicians, has been proved again. According to Quanta Magazine, Mikkel Thorup, a computer scientist at the University of Copenhagen, and Carsten Thomassen, a graph theorist at the Technical University of Denmark, spent close to a decade on the problem with four colleagues in Denmark, Canada and Japan — a group that includes Ken-ichi Kawarabayashi and Bojan Mohar. Their proof was posted online in March 2026 and will be presented in November at the annual Foundations of Computer Science conference.

A simple question with a long history

The theorem asks whether every contiguous map can be colored with four colors so that no two neighboring regions share one. Francis Guthrie hit on the question in 1852 while coloring a map of English counties, and it spread through mathematical circles via his brother's adviser, Augustus De Morgan. The first claimed solution came from Alfred Bray Kempe in 1879, announced in Nature, and stood for eleven years before Percy John Heawood uncovered a subtle flaw.

Kempe's strategy, as Quanta recounts, still shapes the problem. He assumed a minimal map that resisted four-coloring and recast it as a planar graph: countries become vertices and shared borders become edges. A property of planar graphs going back to Euler guarantees that at least one vertex has five or fewer neighbors, which produces an “unavoidable set” of six local configurations. Kempe argued that each of them could always be handled by swapping colors around, so no minimal counterexample could exist. Heawood showed that when the removed vertex has five neighbors, the swapping procedure can leave two identical colors adjacent. Even so, the technique — now known as a Kempe chain — has remained at the core of later work. “Isn't it interesting that you make a mistake which is so interesting that it's named after you?” Thomassen told Quanta.

Why computers had to finish it

A correct proof ultimately required identifying a far larger set of some 8,900 configurations and showing each one reducible, a task Quanta describes as impossible by hand. In 1976, Kenneth Appel and Wolfgang Haken completed the argument with the help of computers, a move considered scandalous at the time and one that forced mathematicians to reconsider what counts as a proof in the first place. The debate largely subsided by 1997, when a simpler computer-assisted proof appeared and the use of computers had become routine.

What the new proof contributes

By one measure, the new argument is even heavier on computation 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 the effort produced two things earlier proofs lacked: a far more efficient way to color maps and graphs, and fresh structural insights into planar graphs. Quanta reports that those insights could open the way to 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.”

Thorup, for his part, calls the lasting pull of the problem the “four-color disease” — he and Thomassen count themselves among the afflicted.

Why it matters

The truth of the four-color theorem has not been in doubt for half a century; what has been missing is understanding. The new work converts brute-force verification into a faster, usable coloring method, and it exposes structural properties of planar graphs that may transfer to other open problems in graph theory. It also traces the arc of computer-assisted proof itself: from a scandal that made mathematicians uneasy in 1976 to an accepted instrument that, wielded with care, can still produce genuinely new mathematics rather than merely reconfirming old results.