Four Color Theorem¶
Every finite loopless planar graph admits a proper vertex coloring with at most four colors.
Core Idea¶
The Four Color Theorem guarantees that every finite loopless undirected planar graph has some proper vertex coloring using at most four colors. All vertices draw from one common palette; endpoints of an edge must receive different labels. The theorem promises that a valid assignment exists, not that every attempted assignment works or that each graph needs exactly four colors.[^ref-d8cbde1e1c9c]
The bound is sharp across the class: the planar complete graph \(K_4\) has four pairwise adjacent vertices, so it needs four different labels. Other planar graphs can need fewer. A proof of the universal theorem is different from a colored example; the inspected Robertson–Sanders–Seymour–Thomas and Gonthier works supply the theorem's published warrant, while the examples below are elementary constructions.[ref-d8cbde1e1c9c][ref-e93a29b030ab]
Scope of Application¶
Apply the guarantee after establishing a finite loopless planar graph and its actual adjacency relation. It can settle the existence of a four-color assignment for a planar conflict graph, including disconnected graphs whose components reuse the same palette. Ordinary connected-region maps can be translated to graphs when the region contacts that count as adjacency are specified.[ref-d8cbde1e1c9c][ref-e93a29b030ab]
A tight example is \(K_4\): draw an outer triangle and one vertex inside it, connected to all three corners. The drawing is planar; four distinct labels give a valid coloring, and all six pairwise edges rule out three labels. A different, nontight example is four open squares in a \(2\times2\) block plus their connected exterior. Side-sharing square pairs and each square–exterior pair form an eight-edge wheel. The central diagonal square pairs meet only at a corner and are not adjacent under the selected map definition. Alternating two labels on the four squares and using a third for the exterior works; a triangle formed by two neighboring squares and the exterior shows that two do not suffice.[^ref-e93a29b030ab]
Clarity¶
At most four is a uniform upper bound, not a per-graph minimum. A failed proposed coloring does not refute an existence theorem: another assignment may work. A small coloring does not prove planarity; the graph's embedding condition must be established separately. Vertex coloring also differs from edge coloring, vertex-specific list coloring, and a guarantee that any greedy order succeeds.
For maps, isolated corner contact is not the same as adjacency in Gonthier's precise connected-open, noncorner formulation. Treating every point contact as a conflict changes the graph. The square example uses an ordinary polygonal map; its side-sharing shorthand is not a definition for every unusual boundary.[^ref-e93a29b030ab]
Manages Complexity¶
Once the proper adjacency graph is fixed, region shapes and literal pigment names disappear from the coloring test. The theorem compresses many individual feasibility questions into one four-label existence guarantee for the entire planar class. It still does not construct a particular assignment in a given application, determine that graph's minimum palette, or settle extra balance, list or preset-label requirements.[^ref-d8cbde1e1c9c]
Abstract Reasoning¶
Check the carrier and premise first: a finite loopless undirected graph must admit a crossing-free drawing. Next ask whether some total assignment from the shared set of four labels can give unequal labels to every edge's endpoints. The theorem answers yes for every graph meeting those premises. An explicit assignment proves an upper bound for one instance; a clique proves a lower bound for that instance. The \(K_4\) and square-map constructions show respectively a tight and a nontight case, without claiming that either finite case proves the universal theorem.
Knowledge Transfer¶
The graph relation transfers literally to a connected-region map when regions become vertices and the selected noncorner contacts become edges. It also transfers to tetrahedron faces, whose pairwise edge-sharing gives the same \(K_4\) adjacency as the tight graph example. Such a change of representation does not create an independent new case. Graph Coloring is the portable conflict-free labeling relation inside this theorem's statement; the exact four-color guarantee additionally needs finiteness, looplessness, planarity and a common palette. The named result is also a Formal theorem, a proved mathematical statement with a specific graph-theoretic differentia.
Relationships to Other Abstractions¶
Current abstraction Four Color Theorem Domain-specific
Parents (2) — more general patterns this builds on
-
Four Color Theorem is a kind of Formal theorem Domain-specific
The Four Color Theorem is a proved mathematical statement with a specific universal planar four-color existence claim.
-
Four Color Theorem is part of Graph Coloring Prime
The proper conflict-free labeling relation is an identity-bearing internal constituent of the theorem's existence statement.
Hierarchy paths (2) — routes to 2 parentless roots
- Four Color Theorem → Formal theorem
- Four Color Theorem → Graph Coloring → Partition → Set and Membership
Neighborhood in Abstraction Space¶
Four Color Theorem sits in a moderately populated region (54th percentile for distinctiveness): it has near-neighbors but no dense thicket of look-alikes.
Family — Graph Structures & Combinatorial Objects (45 abstractions)
Nearest neighbors
- Comparability Graph — 0.88
- Planarity — 0.86
- Geodetic Graph — 0.86
- Biconnected Component — 0.85
- Ordered geometry — 0.85
Computed from structural-signature embeddings · 2026-10-17
References¶
[^ref-d8cbde1e1c9c]: Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas, "The Four-Colour Theorem" (1997), Journal of Combinatorial Theory, Series B 70(1):2–44. DOI: 10.1006/jctb.1997.1750. https://thomas.math.gatech.edu/PAP/fc.pdf. States the theorem in the abstract and §1 and the finite sphere-drawing convention in §2. The inspected source is the 42-page revised author manuscript, cover February 1994, revised 16 January 1997; manuscript pp.1–3 are the locators used here, not the journal pagination. The complete computer case analysis and programs were not independently checked or executed for this account. Exact example coordinates, adjacency lists, assignments and lower bounds above are elementary author constructions.
[^ref-e93a29b030ab]: Georges Gonthier, "Formal Proof—The Four-Color Theorem" (2008), Notices of the American Mathematical Society 55(11):1382–1393. https://www.ams.org/notices/200811/tx081101382p.pdf. States the map theorem on printed p.1383 and the connected-open region, adjacency and corner definitions on printed p.1388, Definitions 2–4. The official article was inaccessible directly; a complete 12-page published-layout facsimile from Cornell was inspected, including the relevant definition page. This is the 2008 published article, distinct from the undated 57-page report A computer-checked proof of the Four Colour Theorem. No Coq proof rerun is claimed. Segment-sharing shorthand is restricted to ordinary polygonal maps; the constructed square example is derived from the published definitions.