New computer-assisted Four-Color proof promises near-linear planar-graph coloring

A team of mathematicians says it has produced a new proof of the Four-Color Theorem — one of mathematics’ most famous settled results — and, with it, a faster way to color planar graphs, the network-like structures that capture the same problem in graph theory. The work is scheduled to be presented next week at the 67th IEEE Symposium on Foundations of Computer Science, or FOCS 2026, in New York City, where the program lists it in the conference’s Best Paper session.

The theorem asks a deceptively simple question: Can any flat map be colored with four colors so that regions sharing a border never get the same color? Mathematicians have known the answer is yes for decades. What makes the new work notable is not that it solves an open problem, but that it offers a new proof with a claimed algorithmic improvement for actually finding such colorings.

The paper, posted to arXiv on March 25, 2026, is titled “The Four Color Theorem with Linearly Many Reducible Configurations and Near-Linear Time Coloring.” Its authors are Yuta Inoue, Ken-ichi Kawarabayashi, Atsuyuki Miyashita, Bojan Mohar, Carsten Thomassen and Mikkel Thorup.

In the paper’s abstract, the authors say they prove a stronger structural result: every planar triangulation — a way of breaking a planar graph into triangular faces — contains linearly many pairwise non-touching reducible configurations, or non-crossing short obstructing cycles. From that, they say, they derive a near-linear-time algorithm, O(n log n), to produce a four-coloring of an n-vertex planar graph.

For non-specialists, the clearest practical meaning is speed. The standard modern proof already implied a way to color planar graphs, but at about O(n²). The new paper says that can be improved to O(n log n), a meaningful reduction for large graphs.

Like the earlier landmark proofs of the theorem, however, this one is still heavily computer-assisted. Quanta Magazine and institutional summaries from the University of Copenhagen’s Basic Algorithms Research Copenhagen, or BARC, said the new proof uses an unavoidable set of 8,202 D-reducible configurations, verified by computer. Those reports said finding and checking the configurations took months of computing, with much of the search and verification done by Inoue and Miyashita, described as Kawarabayashi’s graduate students. Final verification reportedly took hours.

That combination — a major advance, but not the short, purely human-readable proof many mathematicians have long wanted — is part of why the result stands out. “It’s really cool to see a real result for once,” Georges Gonthier said, according to Quanta.

The Four-Color Theorem dates to 1852 and became famous because it is easy to explain but extraordinarily hard to prove. The first accepted proof came in 1976, when Kenneth Appel and Wolfgang Haken used heavy computer assistance to check about 1,482 configurations, helping ignite a long-running debate over computer-assisted proof. The standard modern proof before this came in 1997 from Neil Robertson, Daniel Sanders, Paul Seymour and Robin Thomas. That version still relied on computers, reduced the checked set to 633 configurations and yielded an algorithm of about O(n²).

By comparison, the new result’s main claim is not a simpler proof in the everyday sense. If anything, the reported unavoidable set is much larger. The novelty is in the structure the authors say they establish — linearly many non-touching reducible configurations — and in the faster coloring algorithm that follows.

According to Quanta, the project grew out of a 2015 conversation between Kawarabayashi and Thorup and took nearly a decade. The paper is set for presentation at FOCS in New York from Nov. 8 to Nov. 11. The conference program places it in the Best Paper session. Separately, BARC said in an Oct. 22 news item that the paper “will receive the Best Paper Award at FOCS’26.”

If the claims hold up, mathematicians will have a new benchmark proof of a classic theorem — and a faster algorithm to go with it — but still not the concise, fully human proof that some have hoped for.