TL;DR

The four color theorem says four colors are enough to shade any map so that no two bordering regions match. It is 174 years old, and in 2026 it picked up its first algorithmic speedup in three decades: a planar graph with n vertices can now be 4-colored in O(n log n) time, down from the O(n²) bound Robertson, Sanders, Seymour, and Thomas set in 1996. The paper, by Inoue, Kawarabayashi, Miyashita, Mohar, Thomassen, and Thorup, will appear at FOCS 2026 (New York, November 8-11). Its real content is a structural theorem stronger than the four color theorem itself: every planar triangulation contains linearly many non-touching reducible configurations (or short obstructing cycles), so each round can shrink the graph by a constant factor instead of a constant number of vertices. The proof leans on computer checks over more than 8,200 configurations, and in June the authors published results showing that code written independently by Gemini Deep Think, Claude Code, and OpenAI Codex reproduces those checks. For this article I re-ran two of the lemma checks from the Claude Code version, and both matched.

A Quick History of the Four Color Theorem

The Four Color Theorem says that any map (or equivalently, any planar graph) can be colored with at most four colors so that no two adjacent regions share a color. A schoolchild can state it, and proving it took 124 years and a computer.

Francis Guthrie noticed the pattern in 1852 while coloring a map of English counties. Alfred Kempe published a “proof” in 1879. Percy Heawood found the bug 11 years later. The conjecture then sat open for nearly a century, but Kempe’s failed proof left behind a tool every later proof still uses: the Kempe chain, a connected run of vertices alternating between two colors that you can swap wholesale to free up a color for a stubborn vertex. Keep that idea in mind, because Kempe chains are exactly where the log factor in the 2026 running time comes from.

In 1976, Kenneth Appel and Wolfgang Haken finally proved it by exhaustive computer verification of about 1,500 reducible configurations (1,476 in the standard final count). It was the first major theorem proved by computer, and mathematicians spent decades arguing over whether it counted as a real proof.

In 1996, Robertson, Sanders, Seymour, and Thomas simplified the proof (down to 633 configurations) and produced a quadratic-time coloring algorithm: given a planar graph with n vertices, it finds a valid 4-coloring in O(n²) time. That algorithm held the state of the art for thirty years, until March 2026.

YearAuthorsContributionColoring complexity
1976Appel & HakenFirst proof, ~1,500 configurations checked by computerO(n⁴) coloring
1996Robertson, Sanders, Seymour, ThomasSimplified to 633 configurations + algorithmO(n²)
2026Inoue, Kawarabayashi, Miyashita, Mohar, Thomassen, ThorupProved linearly many reducible configurations exist at onceO(n log n)

What the New Paper Actually Does

The paper is “The Four Color Theorem with Linearly Many Reducible Configurations and Near-Linear Time Coloring” by Yuta Inoue, Ken-ichi Kawarabayashi, Atsuyuki Miyashita, Bojan Mohar, Carsten Thomassen, and Mikkel Thorup. It was posted to arXiv on March 25, 2026 and revised twice since (v2 on May 7, v3 on October 1). The v3 listing notes that a preliminary version will appear at FOCS 2026, the IEEE Symposium on Foundations of Computer Science, one of the two flagship theory conferences.

The headline: O(n log n) time to 4-color any planar graph, down from O(n²). The faster algorithm falls out of a structural theorem about planar graphs that is strictly stronger than the Four Color Theorem itself.

The Old Approach and Why It’s Quadratic

To understand the improvement, you need to understand why the Robertson et al. algorithm is O(n²).

The classic proof strategy works by contradiction. Assume there exists a minimal planar graph that can’t be 4-colored. Then show it must contain at least one “reducible configuration,” a local subgraph pattern that can be simplified while preserving the coloring problem. Simplify it, solve the smaller problem, then extend the coloring back. Since the graph was supposed to be minimal, you have a contradiction.

The algorithm version: scan the graph in linear time and find one reducible configuration (or an obstructing cycle, a short cycle that splits the graph into two parts you can color separately). Shrink it, color the smaller graph recursively, then patch the coloring back onto the removed piece, which may take a few Kempe changes. A single Kempe chain can snake across the whole graph, so that patch step can also cost O(n). Each round removes only O(1) vertices, so you need O(n) rounds at O(n) each. Total: O(n) × O(n) = O(n²).

The bottleneck: the proof only promises one configuration, so you fix it and start scanning all over again.

The New Insight: Linearly Many Configurations at Once

Kawarabayashi, Thorup, and co-authors break through here. They prove that every planar triangulation contains linearly many pairwise non-touching reducible configurations at the same time. Or, alternatively, linearly many short obstructing cycles that also permit effective reductions.

“Linearly many” means Ω(n). A constant fraction of the graph is reducible at any given moment.

Instead of:

  1. Scan the whole graph → find one reduction → apply it → repeat

You get:

  1. Scan the whole graph → find Ω(n) reductions → apply them all at once → repeat

Each round now removes a constant fraction of the vertices, so the graph sizes across rounds form a geometric series: n, then cn, then c²n, and so on for some c < 1. The paper’s §3.1 sets up the recursion this way: build a triangulation smaller by a constant factor in O(n log n) time, color it recursively, then extend the coloring back in another O(n log n). Because the sizes shrink geometrically, the first round dominates and the total is O(n log n).

A common misreading (including an earlier version of this article) attributes the log factor to the number of rounds. The paper puts it somewhere else. Removing all the configurations at once is the easy part. Recoloring is harder: extending the coloring back onto Ω(n) removed pieces needs Kempe changes, and the authors manage it with O(log n) of them per round, each of which can touch a linear number of vertices. That’s O(n log n) per round, and the section heading the authors chose for it, “Bottleneck: the number of Kempe chains,” says where the remaining slack lives. The abstract is blunt about why this took 30 years: such an algorithm “cannot be achieved by the known proofs” of the theorem, because those proofs only ever produce one configuration at a time.

How They Proved It: Curvature and Flat Regions

The classic proof technique for finding reducible configurations is called the discharging method. Think of it like a budget. You assign each vertex and face a “charge” based on its degree. Euler’s formula guarantees that the total charge is positive. You then redistribute (discharge) this charge according to local rules. Vertices that end up with positive charge after discharging must be part of reducible configurations.

In a triangulation, a vertex of degree d carries “curvature” 6 − d: positive for degree 5 or less, zero for degree 6, negative above. Euler’s formula fixes the total at exactly 12, no matter how big the graph is. So the classic argument is guaranteed a fixed, constant amount of positive curvature to work with, and that’s enough to force one reducible configuration, not a growing number of them. The worst case the paper names is a triangulation in which every vertex has degree 6 except for 12 of degree 5. All the positive curvature sits at 12 points and everything else is flat, so a proof that only looks for positive curvature finds a constant number of reductions in a graph of a million vertices.

The new paper extends the discharging method to work in those flat parts too. In the abstract’s words, the authors show “that we can also find reductions in large ‘flat’ parts where the curvature is zero, and moreover, we can make reductions almost anywhere in a given planar graph.” In those zero-curvature areas you can still identify reducible configurations or obstructing cycles of length at most 5, and you can find linearly many of them that don’t interfere with each other. The purely flat case needed a new piece: the classic 6-regular reducible configuration (Franklin’s) is not D-reducible, so the authors found a larger one that is.

All identified configurations are D-reducible, the strongest form of reducibility, where every 4-coloring of the surrounding ring extends into the configuration, either directly or after Kempe changes. That keeps the algorithm fast: D-reducible configurations can be processed in batch, without the more delicate bookkeeping that weaker forms of reducibility (C-reducibility) require, at the cost of needing far more of them. Appel and Haken used roughly 1,500 reducible configurations (the 2026 paper counts 1,482; other sources give 1,476) and Robertson et al. got it down to 633; the new proof uses more than 8,200 D-reducible configurations, and only computers run the local case analysis over all of them.

The Curvature Argument, Run in Python

You can check the “fixed budget of 12” claim on real graphs in a few dozen lines of standard-library Python. The script below builds random planar triangulations: it inserts vertices into random faces, then applies random edge flips so the shape doesn’t stay a lopsided stack. For each graph it prints the total curvature, the degree mix, and a toy version of the batch argument. One round deletes every vertex of degree at most 11 at once. Planar graphs have average degree below 6, so fewer than half the vertices can have degree 12 or more, and each round removes at least half the graph. That caps the number of rounds at about log₂ n.

import math
import random
from collections import Counter

def random_triangulation(n, flips_per_vertex=10, seed=1):
    """Random planar triangulation: random face insertions, then random edge flips."""
    rng = random.Random(seed)
    faces, where = [], {}
    face_of = {}                  # directed edge (a, b) -> the face containing it
    adj = {0: {1, 2}, 1: {0, 2}, 2: {0, 1}}

    def add(f):
        where[f] = len(faces); faces.append(f)
        a, b, c = f
        face_of[a, b] = face_of[b, c] = face_of[c, a] = f

    def drop(f):
        i = where.pop(f); last = faces.pop()
        if last != f:
            faces[i] = last; where[last] = i
        a, b, c = f
        del face_of[a, b], face_of[b, c], face_of[c, a]

    add((0, 1, 2)); add((0, 2, 1))           # two triangles glued: a sphere
    for v in range(3, n):                    # insert v inside a random face
        a, b, c = rng.choice(faces)
        drop((a, b, c))
        add((a, b, v)); add((b, c, v)); add((c, a, v))
        adj[v] = {a, b, c}
        for u in (a, b, c):
            adj[u].add(v)
    for _ in range(flips_per_vertex * n):    # flip edges to mix the shape
        f = rng.choice(faces)
        k = rng.randrange(3)
        u, w, x = f[k], f[(k + 1) % 3], f[(k + 2) % 3]
        g = face_of[w, u]
        y = next(t for t in g if t != u and t != w)
        if x == y or y in adj[x] or len(adj[u]) <= 3 or len(adj[w]) <= 3:
            continue
        drop(f); drop(g)
        add((u, y, x)); add((y, w, x))
        adj[u].discard(w); adj[w].discard(u)
        adj[x].add(y); adj[y].add(x)
    return adj

def batch_rounds(adj, max_deg=11):
    """Peel every vertex of degree <= max_deg at once, count rounds until empty."""
    deg = {v: len(nb) for v, nb in adj.items()}
    alive, rounds = set(adj), 0
    while alive:
        batch = [v for v in alive if deg[v] <= max_deg]
        for v in batch:
            alive.discard(v)
            for u in adj[v]:
                deg[u] -= 1
        rounds += 1
    return rounds

print(f"{'n':>7} {'sum(6-deg)':>10} {'deg<=5':>7} {'deg=6':>6} {'deg>=7':>7} "
      f"{'one-per-scan':>12} {'batch rounds':>12} {'bound':>5}")
for n in (1_000, 10_000, 50_000):
    adj = random_triangulation(n)
    degs = [len(nb) for nb in adj.values()]
    hist = Counter(min(max(d, 5), 7) for d in degs)
    print(f"{n:>7} {sum(6 - d for d in degs):>10} {hist[5] / n:>7.1%} "
          f"{hist[6] / n:>6.1%} {hist[7] / n:>7.1%} {n:>12} {batch_rounds(adj):>12} "
          f"{math.ceil(math.log2(n)) + 1:>5}")

Running it on Python 3.12 (about 9 seconds for all three sizes) prints:

      n sum(6-deg)  deg<=5  deg=6  deg>=7 one-per-scan batch rounds bound
   1000         12   58.6%  11.9%   29.5%         1000            2    11
  10000         12   58.9%  12.1%   29.0%        10000            3    15
  50000         12   58.9%  12.1%   29.0%        50000            3    17

The total curvature is 12 at every size, exactly as Euler’s formula says. Typical random triangulations are far from flat: almost 59% of vertices have degree 5 or less and only about 12% have degree 6, with the positive curvature cancelled out by a long tail of high-degree vertices. The hard case is the near-6-regular graph, which random inputs rarely resemble, but a proof has to cover every planar graph, so the theorem has to handle it anyway. The batch idea pays off even in this toy, finishing in 2-3 rounds where one-at-a-time removal would take n steps, well under the log₂ n guarantee.

The peeling itself is a classic trick from parallel graph coloring (color the layers in reverse and you get a quick 12-coloring). The paper’s algorithm deletes reducible configurations in bulk and must still restore a 4-coloring afterwards, which is what the 8,200 configurations and the Kempe-chain machinery are for.

Three AI Coding Agents Re-Ran the Proof Checks

The four color theorem has always come with an asterisk: part of the proof is a program. Appel and Haken’s 1976 proof drew decades of objections on exactly that point, and the 2026 paper leans even harder on computation, with 84 discharging rules, 8,200 configuration files, and a C++ checker that enumerates every possible neighborhood. The authors publish all of it on GitHub under the near-linear-4ct organization.

In June 2026 they went a step further. A repository called instructions-for-checking-reproducibility lists the key numbers any correct implementation of the paper’s pseudocode should produce. It also includes an instructions file for anyone who wants to write that implementation, by hand or with an LLM. The authors then had three systems write one each: Google Gemini Deep Think, Claude Code, and OpenAI Codex. They report that all three produce the expected values, and they published the generated code. (For the Gemini version, the README notes that the driver script and two shell scripts were written by a human; the library files are Gemini’s.) The Claude Code version ships with its task brief, which let the agent read the C++ repository’s file-format spec and nothing else in it. Its README describes a pure-Python reimplementation of Appendix A.2-A.10 that “deliberately” never consulted the reference code. The paper itself also notes that the authors “asked Gemini to check” the pseudocode and C++, while adding that “using Gemini is no guarantee of correctness.”

The authors’ wording is careful: matching key values “does not guarantee 100% correctness,” but it suggests “no major discrepancies” from the original. I wanted to see whether the published LLM-written code actually runs, so I cloned the Claude Code repository and the two data repositories and ran the first two lemma checks on this machine. Lemma A.1 combines the discharging rules with no configurations excluded:

git clone --depth 1 https://github.com/near-linear-4ct/computer-checks-by-Claude-Code.git cc
git clone --depth 1 https://github.com/near-linear-4ct/discharging-rules.git rules
git clone --depth 1 https://github.com/near-linear-4ct/reducible-configurations.git confs
# no pip install: put the package's src/ on sys.path and call the lemma script directly
python3 -I -c "import sys; sys.path.insert(0, 'cc/src'); \
from four_ct.scripts.check_lemma_a1 import main; \
sys.exit(main(['--rules-dir', 'rules/R', '--quiet']))"

loaded 84 rules from rules/R
combineRules(R, ∅) finished in 32.5s — |R*| = 1832
max r* = 8; achieved by 1 combination(s)

Charge-8 witnesses:
  #1: |V|= 8 |D|= 28 rules (7): rule001, rule002_1, rule002_2, rule003_1, rule003_2, rule004_1, rule004_2

PASS: Lemma A.1 first claim verified — max r* == 8
(Figure-7 isomorphism check is deferred — see plan file.)

Lemma A.2 repeats the combination with the 8,200 D-reducible configurations loaded, so combinations blocked by a reducible configuration drop out (same invocation, check_lemma_a2 plus --confs-dir confs/D):

loading configurations from confs/D...
  |D̂| = 19754 (built in 5.2s)
loaded 84 rules from rules/R
combineRules(R, D̂) finished in 63.2s — |R*⁻D| = 671
max r* = 5; achieved by 10 combination(s)
[... 10 witness lines omitted ...]
PASS: Lemma A.2 first claim verified — max r* == 5
(Figure-8 isomorphism check is deferred — see plan file.)
LemmaQuantityAuthors’ expected valueClaude Code’s Python, run here
A.1Size of R*18321832
A.1Max charge in R*88
A.2Size of R*⁻ᴰ671671
A.2Max charge in R*⁻ᴰ55

Both runs match the authors’ reference table, and together they took under two minutes on a CPU. I didn’t run the cartwheel enumeration (Lemmas A.3-A.6), which is the long tail of the computation. Matching four numbers also doesn’t certify the code’s logic, as the authors themselves say. The script’s own output flags that the Figure-7 and Figure-8 isomorphism parts of these lemmas are “deferred,” so even the LLM version checks only the first claim of each lemma. In 1976 the objection was that no human could check the computer. In 2026, three different AI systems wrote independent checkers from the paper’s text, and anyone can re-run one in a minute. I think that’s more redundancy than most published computer-assisted proofs get. The classic theorem still has a stronger guarantee, Georges Gonthier’s machine-checked proof in the Coq proof assistant, completed in 2005. As far as I could find, nobody has formalized the 2026 result yet. If you follow how these coding models compare on harder engineering work, the ranking of AI models for coding covers the same three vendors.

The Author Lineup

The six authors span graph algorithms and structural graph theory:

  • Mikkel Thorup (University of Copenhagen). Fulkerson Prize 2021, with two decades of foundational results in hashing, shortest paths, and deterministic graph algorithms. His joint work with Kawarabayashi on deterministic edge connectivity was the citation the prize committee leaned on.

  • Ken-ichi Kawarabayashi (National Institute of Informatics, Tokyo), co-winner of the Fulkerson Prize with Thorup, extensive work in graph minors and topological graph theory.

  • Carsten Thomassen (Technical University of Denmark), one of the most prolific graph theorists alive, known for his work on graph coloring and flows. Proved that every planar graph is 5-list-colorable.

  • Bojan Mohar (Simon Fraser University / University of Ljubljana), expert in topological graph theory, graph embedding, and spectral graph theory.

  • Yuta Inoue and Atsuyuki Miyashita (University of Tokyo), who work with Kawarabayashi.

Kawarabayashi and Thorup previously broke the near-linear time barrier for deterministic edge connectivity. Their approach here follows a similar pattern: take a classical problem with a polynomial-time algorithm that everyone assumed was close to optimal, then find structural depth that yields a better bound.

What This Means in Practice

You’re probably not 4-coloring planar graphs in production code. The result still carries lessons beyond the specific algorithm.

For algorithm designers: Finding linearly many independent reductions in a single pass turns an “additive” algorithm into a “multiplicative” one, and the strategy is general. If your algorithm works by repeatedly finding and fixing one local structure, look for a way to find many of them at once. This paper shows that can work even on a famously hard problem.

For complexity theorists: the O(n²) bound was an artifact of the proof technique. It fell once the structural theorem itself got stronger, and similar barriers in other problems might be proof artifacts waiting to be relaxed.

For anyone who appreciates elegant CS: a 174-year-old theorem whose first computer proof is 50 years old and whose best coloring algorithm had stood for 30 years just got meaningfully faster, and the win came from understanding the combinatorial structure better. Graph theory is also where AI keeps showing up in the proof pipeline. A few weeks before this paper appeared, Donald Knuth credited Claude Opus 4.6 with solving an open problem about decomposing a directed graph into Hamiltonian cycles. By June, this paper’s own authors had three coding agents rebuilding their verification code from the pseudocode.

FAQ

Is this a new proof of the Four Color Theorem?

It’s a generalization of the 4CT, which implies the classic theorem as a special case. The classic theorem says every planar triangulation has at least one reducible configuration. This paper says it has linearly many non-touching ones. Finding one is a corollary of finding many.

Has the four color theorem been proven?

Yes. Kenneth Appel and Wolfgang Haken proved it in 1976 with a computer-assisted case analysis, Robertson, Sanders, Seymour, and Thomas published a simpler computer-assisted proof in the late 1990s, and Georges Gonthier completed a fully machine-checked proof in the Coq proof assistant in 2005. The 2026 paper is a fourth route: it proves a stronger statement and gets the classic theorem as a corollary.

Does the algorithm have practical applications?

The gains are mostly theoretical. Map coloring and channel assignment on planar networks are the textbook uses, but practical systems rarely need exactly four colors. Five colors have been achievable in linear time since the early 1980s, and simple greedy heuristics usually do fine on real maps. The paper also cites a limit on parallel speedups: Chechik and Mukhtar showed that 4-coloring planar graphs needs Ω(n) rounds in the distributed LOCAL model, so the Kempe-chain steps can’t be spread across many machines cheaply. The proof technique is likely to outlast this specific algorithm.

Can I run this myself?

You can run the proof checks. The authors publish the C++ computer checks, the rule and configuration files, and the three LLM-generated reimplementations on GitHub. The two Claude Code lemma checks I ran took 32 and 63 seconds on a single CPU core, without a pip install (its one dependency, tqdm, was already on the machine). See the run above. As of October 2026 the authors’ GitHub organization hosts no implementation of the O(n log n) 4-coloring algorithm itself; the configuration-finding and batch Kempe-chain logic is where that engineering work would live.

Why couldn’t the old proofs achieve near-linear time?

The Appel-Haken and Robertson et al. proofs only guarantee one reducible configuration per graph. Removing it reduces the graph by O(1) vertices, so you need O(n) rounds of find-and-reduce. Each round scans the whole graph, which makes the approach inherently quadratic until you have the “linearly many” structural result.

What’s next: can we get linear time?

Nobody knows yet. Since the graph shrinks by a constant factor each round, the round count isn’t the obstacle; the O(log n) factor sits in the recoloring, where each round uses O(log n) Kempe changes that can each cost linear time. Reaching O(n) would mean extending colorings back across all the removed configurations with O(1) such changes per round, or avoiding long Kempe chains altogether, and the paper doesn’t claim either is possible.

The structural results are already being extended. A July 2026 follow-up by Kawarabayashi with Hirotaka and Masataka Yoneda, The Balanced Four-Color Theorem, shows that every planar graph with at least 3 vertices has a 4-coloring in which each color class has fewer than n/2 vertices (which is best possible), and that such a coloring can be found in O(n log n) time.

Sources

Bottom Line

Six authors broke a 30-year-old quadratic barrier by proving that planar graphs have reducible configurations almost everywhere, including in the flat regions every earlier proof skipped. FOCS acceptance plus three independently generated checkers that agree on the published key values make it about as well-supported as a computer-assisted proof gets before anyone formalizes it. I expect the “find linearly many independent local fixes at once” technique to show up in other problems over the next few years. It’s part of a broader run of textbook bounds falling: Dijkstra’s shortest-path algorithm, unbeaten since 1959, recently lost its theoretical crown on sparse directed graphs.