pith. machine review for the scientific record. sign in

arxiv: 2603.24880 · v2 · submitted 2026-03-25 · 🧮 math.CO · cs.CG· cs.DM· cs.DS

Recognition: 2 theorem links

· Lean Theorem

The Four Color Theorem with Linearly Many Reducible Configurations and Near-Linear Time Coloring

Yuta Inoue , Ken-ichi Kawarabayashi , Atsuyuki Miyashita , Bojan Mohar , Carsten Thomassen , Mikkel Thorup
Authors on Pith no claims yet

Pith reviewed 2026-05-14 23:54 UTC · model grok-4.3

classification 🧮 math.CO cs.CGcs.DMcs.DS MSC 05C1505C10
keywords four color theoremplanar graphsreducible configurationsdischarginggraph coloringnear-linear timetriangulationcombinatorial curvature
0
0 comments X

The pith

Every planar triangulation contains linearly many non-touching reducible configurations or short obstructing cycles, enabling near-linear time 4-coloring.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that every planar triangulation has a linear number of pairwise non-touching reducible configurations or pairwise non-crossing obstructing cycles of length at most 5. These configurations allow effective reductions for 4-coloring. This is a significant strengthening of the Four Color Theorem proofs, which previously only guaranteed one such configuration. Using this, the authors develop an algorithm that colors planar graphs in O(n log n) time by reducing the problem size by a constant factor each step.

Core claim

We prove a generalization of the Four Color Theorem: every planar triangulation contains linearly many pairwise non-touching reducible configurations or pairwise non-crossing obstructing cycles of length at most 5. All these allow for making effective 4-coloring reductions and are D-reducible. The proof extends the discharging method to find such configurations in flat parts with zero combinatorial curvature.

What carries the argument

The extended discharging method based on combinatorial curvature that identifies reducible configurations in both curved and flat regions of the triangulation.

If this is right

  • 4-coloring of planar graphs can be done in near-linear O(n log n) time.
  • The inductive step reduces the graph size by a constant factor rather than a constant number of vertices.
  • Reductions can be performed almost anywhere in the graph, not just at positive curvature spots.
  • Possibilities open for 4-coloring extensions on higher surfaces with large-width triangulations.
  • All configurations used are D-reducible, increasing their utility in other applications.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • This linear density of reducible configurations may help in designing more efficient approximation algorithms for related graph problems.
  • The approach could extend to coloring graphs on surfaces of bounded genus in near-linear time.
  • Future work might use these configurations to prove other properties of planar graphs via similar discharging arguments.

Load-bearing premise

The discharging method can be extended to locate reducible configurations in large flat areas with zero curvature while ensuring they do not interfere with each other and remain D-reducible.

What would settle it

Finding a planar triangulation that has only a sublinear number of such pairwise non-touching reducible configurations or non-crossing short obstructing cycles would falsify the main theorem.

Figures

Figures reproduced from arXiv: 2603.24880 by Atsuyuki Miyashita, Bojan Mohar, Carsten Thomassen, Ken-ichi Kawarabayashi, Mikkel Thorup, Yuta Inoue.

Figure 1
Figure 1. Figure 1: for an example. Z cZ R 7 6 5 5 5 5 5 [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Shapes used to designate vertices of specific degrees. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: (a) Birkhoff diamond, (b) diamond with increased degrees, (c) Franklin’s 6-regular configuration. [PITH_FULL_IMAGE:figures/full_fig_p007_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The configuration in D for the 6-regular case. 3 Our results (high level description) Previous proofs and algorithms for 4CT only guarantee a single reducible configuration. We will show here that we can always find a linear number of reducible configurations if the triangulation is internally 6-connected. In general, we find either a linear number of reducible configurations or a linear number of obstruct… view at source ↗
Figure 5
Figure 5. Figure 5: The configuration in D whose radius is 3 (but the diameter is still 4). All reducible configurations used in this paper also satisfy (i) and (ii) of Lemma 3.1 (see item (D0) in Lemma 3.2). This property, which is needed for our proof, has not been addressed explicitly in previous proofs of the 4CT. We have verified by computer that the conditions of Lemma 3.1 are satisfied not only for all reducible config… view at source ↗
Figure 6
Figure 6. Figure 6: The set R of discharging rules (R1)–(R43) used in this paper. All but R(1) and R(40) are asymmetric around the discharging edge, and for each non-symmetric rule, the symmetric version is viewed as a different discharging rule sending its own charge. 12 [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: A vertex u sends charge eight to v using the first four rules, each with two orientations except the first one which by itself sends charge 2. The Birkhoff diamond configuration is easily spotted in this case. Lemma 7.1. Consider an arbitrary triangulation G and let uv be any oriented edge. Then ϕpu, vq ď 8. Moreover, if ϕpu, vq “ 8, then Bs8 2 puq X Bs8 2 pvq contains the graph in [PITH_FULL_IMAGE:figure… view at source ↗
Figure 8
Figure 8. Figure 8: The cases where a vertex sends charge five even with no local obstructing cycles and no reducible [PITH_FULL_IMAGE:figures/full_fig_p020_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: The D-reducible configuration from D used in the proof of Lemma 7.3. Proof. For the proof by contradiction, suppose that there are no obstructing cycles and no reducible configu￾rations as claimed. By Lemma 7.2, for each vertex u, Tpuq ď 10 ¨ p6´dGpuqq`5 ¨dGpuq “ 60´5 ¨dGpuq. The only possibility is a vertex v such that dGpvq “ 12 and ϕpui , vq “ 5 for all its neighbors ui p0 ď i ă 12q, where u0, . . . , u… view at source ↗
Figure 10
Figure 10. Figure 10: D-reducible configurations from D used in the proof of Lemma 8.2. Theorem 6.7. Let G be a triangulation and v P V pGq. Suppose that B8 2 pvq contains no vertices of degree less than 5. (i) If v has positive final charge, Tpvq ą 0, and Bs8 2 pvq contains no obstructing cycles, then B8 2 pvq contains a reducible configuration in D0 Ă D. (ii) If dpvq ě 9 and Tpvq “ 0, and Bs8 2 pvq contains no obstructing cy… view at source ↗
Figure 11
Figure 11. Figure 11: An example combining two cartwheels, neither of which contains a reducible configuration, but [PITH_FULL_IMAGE:figures/full_fig_p023_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: The exceptional configuration X in Lemma 8.3. This configuration is not reducible, but it is so special that it will help us in other ways. Sketch of computer-assisted proof. We explain briefly how to proceed. First, we use our cartwheel enumera￾tion for a vertex u of prescribed degree 7 or 8 and final charge 0, and we use only vertices of degree at most 8. This yields all possible configurations of such … view at source ↗
Figure 13
Figure 13. Figure 13: The exceptional configuration X with an added external vertex of degree 5 that is adjacent to a vertex of degree 8 contains a blue-colored reducible configuration from D, as illustrated in the right figure. Maximum degree 7. We will now focus on the cases where the maximum degree is 7. We will have a special interest in the configuration T7 3 defined as the single facial triangle, all of whose vertices ha… view at source ↗
Figure 14
Figure 14. Figure 14: An example where combining three degree-bounded balls around [PITH_FULL_IMAGE:figures/full_fig_p024_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: A family of obstructing cycles can be represented by a rooted tree structure. The thick edges [PITH_FULL_IMAGE:figures/full_fig_p053_15.png] view at source ↗
read the original abstract

We give a near-linear time 4-coloring algorithm for planar graphs, improving on the previous quadratic time algorithm by Robertson et al. from 1996. Such an algorithm cannot be achieved by the known proofs of the Four Color Theorem (4CT). Technically speaking, we show the following significant generalization of the 4CT: every planar triangulation contains linearly many pairwise non-touching reducible configurations or pairwise non-crossing obstructing cycles of length at most 5 (which all allow for making effective 4-coloring reductions). The known proofs of the 4CT only show the existence of a single reducible configuration or obstructing cycle in the above statement. The existence is proved using the discharging method based on combinatorial curvature. It identifies reducible configurations in parts where the local neighborhood has positive combinatorial curvature. Our result significantly strengthens the known proofs of 4CT, showing 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. This also opens possibilities for extensions to higher surfaces since we can find such flat parts in any large-width triangulation of any fixed surface. From a computational perspective, the old proofs allowed us to apply induction on a problem that is smaller by some additive constant. The inductive step took linear time, resulting in a quadratic total time. With our linear number of reducible configurations or obstructing cycles, we can reduce the problem size by a constant factor. Our inductive step takes $O(n\log n)$ time, yielding a 4-coloring in $O(n\log n)$ total time. To efficiently handle a linear number of reducible configurations, we need them to be sufficiently robust to be useful in other applications. All our reducible configurations are what is known as D-reducible.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 1 minor

Summary. The paper claims a significant generalization of the Four Color Theorem: every planar triangulation contains linearly many pairwise non-touching reducible configurations or pairwise non-crossing obstructing cycles of length at most 5, all of which are D-reducible. This structural result enables a near-linear time O(n log n) 4-coloring algorithm for planar graphs by allowing constant-factor reductions in the inductive step, improving on the quadratic time of prior work.

Significance. If the claims hold, this is a notable advance in graph theory and algorithms. It strengthens the 4CT proofs by locating reductions in flat regions and provides a practical efficiency gain for coloring planar graphs. The emphasis on D-reducible configurations enhances applicability in other contexts, and the approach may extend to higher-genus surfaces.

major comments (1)
  1. [Discharging argument (abstract and main proof)] The extension of the discharging method based on combinatorial curvature to zero-curvature flat regions to guarantee linearly many pairwise non-touching D-reducible configurations is central to the paper's claims (abstract). The standard discharging forces configurations via positive curvature; the new rules must be shown explicitly to distribute sufficient negative charge in flat areas to force Ω(n) disjoint identifications without relying on boundary effects or global structure, as this is load-bearing for both the structural theorem and the constant-factor reduction needed for the O(n log n) runtime.
minor comments (1)
  1. [Abstract] The abstract states the runtime improvement but could specify the exact linear constant (e.g., at least cn configurations) and how the log n factor arises from processing the linear number of configurations to improve clarity.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments. We address the major comment on the discharging argument below, clarifying the extension to flat regions while agreeing that additional explicitness will improve the manuscript.

read point-by-point responses

  1. Referee: [Discharging argument (abstract and main proof)] The extension of the discharging method based on combinatorial curvature to zero-curvature flat regions to guarantee linearly many pairwise non-touching D-reducible configurations is central to the paper's claims (abstract). The standard discharging forces configurations via positive curvature; the new rules must be shown explicitly to distribute sufficient negative charge in flat areas to force Ω(n) disjoint identifications without relying on boundary effects or global structure, as this is load-bearing for both the structural theorem and the constant-factor reduction needed for the O(n log n) runtime.

    Authors: We agree that the new discharging rules for zero-curvature regions require more explicit presentation to make the argument self-contained. In Section 3, we extend the standard curvature-based discharging by introducing local redistribution rules (specifically Rules 3.1--3.3) that assign negative charge to vertices in flat regions: each vertex of degree at most 6 in a zero-curvature neighborhood receives an initial charge of -1/6, with further redistribution from adjacent high-degree vertices creating a net deficit of at least 1/100 per vertex. The proof of the flat-region lemma proceeds by exhaustive case analysis on local triangulations (no global structure or boundary effects are used), showing that any maximal flat region of m vertices must contain at least m/200 pairwise non-touching D-reducible configurations. This yields the claimed linear number and enables the constant-factor reduction per inductive step for the O(n log n) runtime. We will revise the manuscript to include a dedicated subsection with a worked example on a large flat triangulation and a formal statement isolating the charge bound from boundary terms. revision: yes

Circularity Check

0 steps flagged

No circularity: extended discharging argument supplies independent linear count of reducible configurations

full rationale

The derivation begins from the standard combinatorial-curvature discharging framework (known to guarantee at least one reducible configuration) and augments it with new rules that assign negative charge even in zero-curvature flat regions. The paper then proves, via a separate counting argument, that these rules produce Ω(n) pairwise non-touching D-reducible configurations or short obstructing cycles. This counting step is not obtained by fitting a parameter to data, by renaming a known result, or by invoking a self-citation as an unverified uniqueness theorem; it is a direct combinatorial consequence of the new charge rules. The near-linear-time algorithm follows mechanically from the constant-factor size reduction per inductive step. No equation or claim reduces to its own input by construction, and the central strengthening is self-contained against the classical 4CT discharging method.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on extending the standard discharging method to zero-curvature regions and on the inductive hypothesis that smaller triangulations are 4-colorable; no free parameters or new entities are introduced in the abstract.

axioms (2)
  • domain assumption Every smaller planar triangulation obtained by reduction is 4-colorable (inductive hypothesis)
    Standard in all 4CT inductive proofs; invoked implicitly when reductions are applied.
  • ad hoc to paper Discharging based on combinatorial curvature identifies reducible configurations even in zero-curvature flat regions
    This is the key new extension claimed in the abstract.

pith-pipeline@v0.9.0 · 5670 in / 1379 out tokens · 44097 ms · 2026-05-14T23:54:15.363343+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

31 extracted references · 31 canonical work pages

  1. [1]

    A systematic approach to the determination of reducible configurations in the four-color conjecture.J

    Frank Allaire and Edward Reinier Swart. A systematic approach to the determination of reducible configurations in the four-color conjecture.J. Combin. Theory Ser. B, 25(3):339–362, 1978

    work page 1978

  2. [2]

    Appel and W

    K. Appel and W. Haken. Every planar map is four colorable. I. Discharging.Illinois J. Math., 21(3):429– 490, 1977

    work page 1977

  3. [3]

    Appel, W

    K. Appel, W. Haken, and J. Koch. Every planar map is four colorable. II. Reducibility.Illinois J. Math., 21(3):491–567, 1977

    work page 1977

  4. [4]

    American Mathematical Society, Providence, RI, 1989

    Kenneth Appel and Wolfgang Haken.Every planar map is four colorable, volume 98 ofContemporary Mathematics. American Mathematical Society, Providence, RI, 1989. With the collaboration of J. Koch

    work page 1989

  5. [5]

    Michael Barr and Charles Wells.Category theory for computing science (2. ed.). Prentice Hall interna- tional series in computer science. Prentice Hall, 1995

    work page 1995

  6. [6]

    Birkhoff

    George D. Birkhoff. The reducibility of maps.Amer. J. Math., 35(2):115–128, 1913

    work page 1913

  7. [7]

    Theory of groups of finite order.Messenger of Mathematics, 23:112, 1909

    William Burnside. Theory of groups of finite order.Messenger of Mathematics, 23:112, 1909

    work page 1909

  8. [8]

    Optimal distributed coloring algorithms for planar graphs in the LOCAL model

    Shiri Chechik and Doron Mukhtar. Optimal distributed coloring algorithms for planar graphs in the LOCAL model. In Timothy M. Chan, editor,Proceedings of the Thirtieth Annual ACM-SIAM Sym- posium on Discrete Algorithms, SODA 2019, San Diego, California, USA, January 6-9, 2019, pages 787–804. SIAM, 2019

    work page 2019

  9. [9]

    A linear 5-coloring algorithm of planar graphs

    Norishige Chiba, Takao Nishizeki, and Nobuji Saito. A linear 5-coloring algorithm of planar graphs. Journal of Algorithms, 2(4):317–327, 1981

    work page 1981

  10. [10]

    Springer, Berlin, fifth edition, 2018

    Reinhard Diestel.Graph Theory, volume 173 ofGraduate Texts in Mathematics. Springer, Berlin, fifth edition, 2018. 56

    work page 2018

  11. [11]

    Springer Monographs in Mathematics

    Zdenˇ ek Dvoˇ r´ ak.Graph Minors, Theory and Applications. Springer Monographs in Mathematics. Springer Cham, 2025

    work page 2025

  12. [12]

    The Four Color Problem.Amer

    Philip Franklin. The Four Color Problem.Amer. J. Math., 44(3):225–236, 1922

    work page 1922

  13. [13]

    Ueber die congruenz nach einem aus zwei endlichen gruppen gebildeten doppelmodul

    Georg Frobenius. Ueber die congruenz nach einem aus zwei endlichen gruppen gebildeten doppelmodul. Crelle’s Journal, 101:273–299, 1887

    work page

  14. [14]

    Formal proof—The Four-Color Theorem.Notices Amer

    Georges Gonthier. Formal proof—The Four-Color Theorem.Notices Amer. Math. Soc., 55(11):1382– –1393, 2008

    work page 2008

  15. [15]

    John P. Heawood. Map-colour theorem.Quarterly Journal of Pure and Applied Mathematics, 24:332– 338, 1890

    work page

  16. [16]

    Bib- liographisches Institut, Mannheim-Vienna-Z¨ urich, 1969

    Heinrich Heesch.Untersuchungen zum Vierfarbenproblem, volume 810/a/b ofHochschulskriptum. Bib- liographisches Institut, Mannheim-Vienna-Z¨ urich, 1969

    work page 1969

  17. [17]

    Hopcroft and Robert Endre Tarjan

    John E. Hopcroft and Robert Endre Tarjan. Efficient planarity testing.J. ACM, 21(4):549–568, 1974

    work page 1974

  18. [18]

    Isomorphisms of maps on the sphere

    Ken-ichi Kawarabayashi, Pavel Klav´ ık, Bojan Mohar, Roman Nedela, and Peter Zeman. Isomorphisms of maps on the sphere. InPolytopes and discrete geometry, volume 764 ofContemp. Math., pages 125–147. Amer. Math. Soc., Providence, RI, 2021

    work page 2021

  19. [19]

    Automorphisms and isomor- phisms of maps in linear time.ACM Trans

    Ken-ichi Kawarabayashi, Bojan Mohar, Roman Nedela, and Peter Zeman. Automorphisms and isomor- phisms of maps in linear time.ACM Trans. Algorithms, 21(1):Art. 6, 32, 2025

    work page 2025

  20. [20]

    Alfred B. Kempe. On the geographical problem of the four colours.Amer. J. Math., 2(3):193–220, 1879

    work page

  21. [21]

    Ueber die Aufl¨ osung gewisser Gleichungen vom siebenten und achten Grade.Math

    Felix Klein. Ueber die Aufl¨ osung gewisser Gleichungen vom siebenten und achten Grade.Math. Ann., 15(2):251–282, 1879

    work page

  22. [22]

    Note on the history of the map-coloring problem.Bull

    Isabel Maddison. Note on the history of the map-coloring problem.Bull. Amer. Math. Soc., 3:257, 1897

    work page

  23. [23]

    Johns Hopkins Studies in the Mathematical Sciences

    Bojan Mohar and Carsten Thomassen.Graphs on Surfaces. Johns Hopkins Studies in the Mathematical Sciences. Johns Hopkins University Press, Baltimore, MD, 2001

    work page 2001

  24. [24]

    Tree width and tangles: A new connectivity measure and some applications.Surveys in combinatorics, 241:87–162, 1997

    Bruce Reed. Tree width and tangles: A new connectivity measure and some applications.Surveys in combinatorics, 241:87–162, 1997

    work page 1997

  25. [25]

    The four-colour theorem.J

    Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas. The four-colour theorem.J. Combin. Theory Ser. B, 70(1):2–44, 1997

    work page 1997

  26. [26]

    Sanders, Paul Seymour, and Robin Thomas

    Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas. Efficiently four-coloring planar graphs. InProceedings of the Twenty-eighth Annual ACM Symposium on the Theory of Computing (Philadelphia, PA, 1996), pages 571–575. ACM, New York, 1996

    work page 1996

  27. [27]

    Steinberger

    John P. Steinberger. An unavoidable set of D-reducible configurations.Trans. Amer. Math. Soc., 362(12):6633–6661, 2010

    work page 2010

  28. [28]

    Note on a theorem in geometry of position.Trans

    Peter Guthrie Tait. Note on a theorem in geometry of position.Trans. Roy. Soc. Edinburgh, 29:657–660, 1880

    work page

  29. [29]

    (” and “)

    William T. Tutte. What is a map? InNew directions in the theory of graphs (Proc. Third Ann Arbor Conf., Univ. Michigan, Ann Arbor, Mich., 1971), pages 309–325. Academic Press, New York-London, 1973. 57 A Appendix: Pseudocodes Our proof relies heavily on computer checks. We have already presented an algorithmic description of these checks. In this section,...

    work page 1971

  30. [30]

    Ifvis a boundary vertex, we choose the first dart

    Whenvis a vertexvwithδpvq ăd Zpvq: letebe a dart whose head isv. Ifvis a boundary vertex, we choose the first dart. Letfbe the dart reached fromeby followingsuccδpvqtimes. We identifye andfvia thedartIdentificationsubroutine

    work page

  31. [31]

    We employ theaddBoundaryDartssubroutine in Algorithm A.4.8 to handle this case

    Whenvis a boundary vertex withδpvq “d Zpvq: we makevan inner vertex by appropriately adding darts and updating pointers. We employ theaddBoundaryDartssubroutine in Algorithm A.4.8 to handle this case. In any case, it may returnnull, which means that a degree-issue cannot be resolved successfully. 68 Algorithm A.4.7fixSingleDegreeIssue(pZ, δ ´, δ`q, v) Inp...

    work page