Four Color Theorem¶

Every finite loopless planar graph admits a proper vertex coloring with at most four colors.

Version: v1 · 2026-10-17 · History
Domain-specific #: 14158
Domain group: Formal Sciences
Origin domain: Mathematics
Subdomain: Graph Theory → Mathematics
Aliases: Four Colour Theorem, Four-Color Theorem, Four-Colour Theorem

Core Idea¶

The Four Color Theorem guarantees that every finite loopless undirected planar graph has some proper vertex coloring using at most four colors. A color is a label: each vertex receives one, and the endpoints of each edge receive different labels. The palette is common to all vertices. The theorem promises that a suitable assignment exists; a particular attempted assignment can still fail.^[1]

The revised Robertson–Sanders–Seymour–Thomas proof organizes 633 configurations through reducibility and unavoidability arguments. Gonthier's published formal-proof account separately explains how a formal combinatorial result is connected to the intended topological map statement. These are grounds for the guarantee, distinct from the graph conditions to which it applies.^[1]^[2]

The numeral four is a uniform upper bound over this graph class. Some members need fewer colors, while the planar complete graph on four vertices needs all four. Its tightness follows from the elementary construction below: all four vertices are pairwise adjacent, so no pair can reuse a label. The theorem therefore concerns a bound across a class, rather than a claim that every individual graph has the same minimum.

For ordinary polygonal maps, connected regions can be represented by vertices and their relevant shared boundaries by edges. This translation needs an adjacency convention. In Gonthier's precise formulation, a simple map has pairwise-disjoint connected open regions; two regions are adjacent when their closures share a point that is not a corner, and a corner lies in the closures of at least three regions. Shared-segment versus isolated-corner language is a useful shorthand for ordinary finite polygonal decompositions, rather than a definition for every pathological topological boundary.^[2]

Structural Signature¶

Sig role-phrases:

Finite loopless undirected graph. A finite vertex set and its undirected edges supply the objects and constraints. A loop is excluded because it would require a vertex's label to differ from itself. Parallel edges are permitted by the source convention and repeat the same endpoint inequality.^[1]
Planarity premise. The graph admits a drawing without edge crossings away from common endpoints, in the plane or on a sphere. This is a property of possible embeddings; a crossing in one poorly chosen drawing does not settle it. Planarity is a hypothesis of the guarantee.^[1]
Specified adjacency relation. Each edge fixes a pair that must receive unequal labels. In a map representation, changing which contacts count changes those constraints. In the precise simple-map formulation, mere corner contact does not supply adjacency.^[2]
Common palette of at most four labels. The same four-element label set is available at every vertex. Some labels may be unused. This differs from supplying each vertex with its own independently prescribed list or imposing additional balance conditions.^[1]
Proper total vertex assignment. Every vertex receives a palette label, and every edge has differently labeled endpoints. A partial assignment or an assignment with a monochromatic edge does not witness the conclusion.
Universal existence guarantee. For every graph satisfying the carrier and planarity premises, with its specified adjacency, there exists a proper total assignment from the common palette. The assignment is the conclusion of the theorem, not an additional premise that must already be established.^[1]

These roles describe a mathematical statement. Computers, a particular coloring algorithm and the configurations used in a proof are not constituents of every graph to which the theorem applies.

What It Is Not¶

Not approval of any four-label assignment. The quantifier is there exists a proper assignment. Giving both endpoints of an edge the same label remains invalid even when another assignment would work.
Not a demand to use exactly four colors. An admissible graph colored with two or three labels also satisfies the conclusion. Four is needed as a bound for the whole class because tight instances exist.
Not a converse test for planarity. A small palette does not itself establish a crossing-free embedding. The hypothesis must be checked separately.
Not edge coloring. Here vertices receive labels and adjacent vertices differ. Assigning labels to edges subject to a different conflict relation is a different problem.
Not a guarantee for every stronger coloring requirement. Arbitrary vertex-specific lists, equal-sized color classes, prescribed vertex labels or a mandated greedy order add conditions absent from the statement. Their feasibility does not follow merely from this theorem.
Not a rule that all touching map regions differ. The selected map formulation excludes corner-only contact. Adding those contacts as edges can create a different, nonplanar conflict graph.^[2]
Not the history or method of its proof. The theorem is the quantified guarantee. A proof establishes it; one colored picture illustrates an instance.

Scope of Application¶

The guarantee has several literal mathematical uses:

Finite planar vertex-color feasibility. Once a finite loopless graph is known to be planar, four common labels suffice to satisfy its vertex-adjacency inequalities.^[1]
Ordinary connected-region maps. A finite polygonal region decomposition can be analyzed through its specified adjacency graph. Side-sharing and isolated corner meetings must be distinguished, as in the square-and-exterior example below.^[2]
Sphere-type face-color translations. Tetrahedron faces furnish a concrete case: each face shares an edge with every other face, giving the same complete four-vertex adjacency graph used below. This is a change of representation of one structure, not an extra independent example.
Disconnected finite graph assemblies. Admissible components can reuse the same palette. Their assignments combine because there are no edges between components; the number of components does not require a separate four-color palette for each.

A geographic name does not establish connectedness. Several disconnected pieces required to share one political label introduce an extra constraint. Similarly, calling a conflict problem a layout, frequency plan or polyhedron does not by itself establish planar adjacency. The actual graph and its premises determine whether the bound applies.

Clarity¶

The theorem separates three questions that the word coloring can blur: Which pairs must differ? Does a valid assignment exist within this palette? What is the smallest palette for this particular graph? The Four Color Theorem answers the second question for the stated planar class. It supplies an upper bound for the third without determining every individual minimum.

It also separates a failed witness from a false existence claim. If a proposed coloring has a monochromatic edge, the proposal fails. That observation alone does not challenge the theorem: another assignment can satisfy all inequalities. A counterexample to the theorem would need to satisfy its graph premises while admitting no proper four-coloring.

For maps, the same discipline resolves a visual ambiguity. Four squares can all meet at a center without all being pairwise adjacent in the relevant sense. The central point is a corner; the shared side interiors supply the actual adjacency constraints. Thus a crowded point in the drawing need not demand a new color for every meeting region.^[2]

Manages Complexity¶

A finite planar graph can contain many vertices and edges. The theorem replaces a separate palette-existence question for every such graph with one uniform conclusion: four labels suffice. It does not require the reader to know every degree, face shape or edge count before using that upper bound, provided the graph premises are established.^[1]

The map translation performs a different compression. Once the correct region-adjacency graph is fixed, literal pigments, region areas and the exact shapes of ordinary polygonal boundaries are not additional coloring constraints. What remains relevant is which vertex pairs must differ. The translation is useful only if it preserves the intended contacts; erasing the distinction between a shared side and a corner changes the problem being compressed.^[2]

The remaining tasks stay separate. Establishing planarity, finding a particular assignment, verifying its edge inequalities and determining its minimum palette are different questions. A general existence theorem settles neither an arbitrary attempted coloring nor every extra requirement an application may impose.

Abstract Reasoning¶

Let $\mathcal P_{\mathrm{fin,loopless}}$ be the class of finite loopless undirected planar graphs. For $G=(V,E)$ in that class, $V$ is the vertex set, $E$ is the edge collection and $c$ a total label assignment. Each edge has an unordered pair of distinct endpoints. Parallel edges may repeat one endpoint pair and therefore repeat the same inequality. The theorem states

\[ \forall G\in\mathcal P_{\mathrm{fin,loopless}},\quad \exists c:V(G)\to\{1,2,3,4\},\quad \forall uv\in E(G),\ c(u)\ne c(v). \]

The graph convention and this at-most-four existence statement are those of the revised Robertson–Sanders–Seymour–Thomas manuscript; the displayed quantifiers explicitly unpack them.^[1]

The inference runs from the graph's premises to the existence of an assignment. The coloring need not be known before the inference is licensed. Conversely, producing a coloring of one graph supplies a witness for that graph, not a proof of the universal statement. The empty graph has the empty assignment, and disconnected components can reuse the common labels: both follow directly from the absence of additional edge inequalities.

Upper and lower bounds answer different questions. A displayed proper assignment using $k$ labels proves that no more than $k$ are needed for that instance. A set of $k$ pairwise adjacent vertices proves that at least $k$ are needed. In the examples below, matching bounds establish four for $K_4$ and three for the square-plus-exterior map. Neither derivation relies on guessing that every planar graph attains the theorem's bound.

Knowledge Transfer¶

Literal transfer begins by preserving the graph relation. A map region becomes a vertex, and a relevant contact becomes an edge; a proper vertex assignment then gives region labels that differ where required. The four square interiors and their exterior make this translation explicit. Tetrahedral face adjacency gives a second representation of the complete graph case. The labels change their physical interpretation while the inequalities remain the same.

Transfer can fail at the modeling step. Combining disconnected regions under one required color, counting every point contact as a conflict or moving to a surface whose adjacency graph is not planar changes the premise or constraints. The universal bound cannot simply be carried across those changes.

The broader transferable pattern is Graph Coloring: conflict-free labeling under pairwise separation constraints. The Four Color Theorem supplies one exact guarantee within that pattern. A scheduling or frequency problem may be a literal coloring problem, but its four-label feasibility still needs the theorem's planar-graph premises rather than a resemblance to a drawn map.

Examples¶

Canonical: a tight planar complete graph¶

This is an elementary construction from the theorem's graph definitions. Take four vertices $a,b,c,d$ and all six edges between distinct pairs. Draw $a=(0,0)$, $b=(2,0)$ and $c=(1,2)$ as an outer triangle, with $d=(1,\tfrac12)$ strictly inside. The three triangle edges and the three edges from $d$ to the outer vertices meet only at common endpoints, so the drawing is planar. It is a finite loopless instance of the graph class in the theorem.^[1]

Assign $c(a)=1$, $c(b)=2$, $c(c)=3$ and $c(d)=4$. All six edge inequalities hold. Because every pair of vertices is adjacent, all four labels must differ; fewer than four cannot work. The displayed assignment proves the upper bound, the complete adjacency proves the lower bound, and together they establish that this instance needs exactly four colors. This is an author derivation, not a claim that the source printed these coordinates or reported an experiment.

The four triangular faces of a tetrahedron have the same pairwise shared-edge adjacency. Giving each face a different color is therefore a representation of this same $K_4$ case. It does not supply a third unlike construction.

Mapped back: Finite loopless undirected graph — four vertices and six edges; Planarity premise — the explicit triangle-and-interior drawing; Specified adjacency relation — every distinct pair is an edge; Common palette of at most four labels — labels $1,2,3,4$ are available to every vertex; Proper total vertex assignment — the four displayed distinct labels satisfy every edge; Universal existence guarantee — the source-established theorem applies to this admissible graph, while the separate clique argument shows that the uniform bound is sharp. This one assignment does not prove the universal theorem.

Applied/practice: four squares and a connected exterior¶

Consider the following explicit ordinary polygonal map, constructed using the connected-open and noncorner definitions of a simple map.^[2]

\[ \begin{aligned} a&=(0,1)\times(0,1), & b&=(1,2)\times(0,1),\\ c&=(0,1)\times(1,2), & d&=(1,2)\times(1,2),\\ o&=\mathbb R^2\setminus([0,2]\times[0,2]). \end{aligned} \]

These five regions are pairwise disjoint connected open sets. The four inner regions share sides in the cycle $a-b-d-c-a$, and the exterior $o$ shares an outer boundary segment with each. The eight adjacency edges are therefore

\[ ab,\ bd,\ dc,\ ca,\ oa,\ ob,\ oc,\ od. \]

The diagonal pairs $a,d$ and $b,c$ meet only at $(1,1)$. That point lies in all four inner closures and is a corner, so neither diagonal pair is adjacent under the stated definition. The midpoint of an inner shared side belongs to only its two neighboring closures and supplies a noncorner contact. This is an explicit derivation from the published definitions, rather than a claimed transcription of a colored source figure.^[2]

The adjacency graph is planar: draw the four-cycle as a diamond and place $o$ at its center, joining it to every cycle vertex. The graph drawing need not put the exterior-region vertex outside the cycle; it represents adjacency, not the regions' literal coordinates. Assign $a=d=1$, $b=c=2$ and $o=3$. Every listed edge has different endpoint labels. The triangle $a,b,o$ rules out two colors, so the explicit assignment and lower bound establish a minimum of three. The theorem's palette of four remains sufficient with one unused label.

If both central diagonal contacts were instead added as conflicts, the four inner vertices would form a complete graph and the exterior would conflict with all four. The result would be $K_5$, requiring five distinct labels. That is a different adjacency problem, not a failure of the stated theorem.

Mapped back: Finite loopless undirected graph — the five region vertices and eight listed edges; Planarity premise — the explicit wheel embedding; Specified adjacency relation — side contacts and exterior contacts, excluding the central corner-only diagonal pairs; Common palette of at most four labels — the same labels $1,2,3,4$ are available throughout; Proper total vertex assignment — $a=d=1$, $b=c=2$, $o=3$ satisfies all eight edges; Universal existence guarantee — the theorem covers this graph, and the elementary construction demonstrates a nontight instance using three labels. Neither the map nor its coloring is an independent empirical validation of the theorem.

Structural Tensions¶

The theorem does not impose competing objectives that must be traded against one another. Planarity is a hypothesis, properness is a constraint and four is an exact uniform upper bound. Using only three colors in one example does not pull against the theorem; it satisfies an at-most-four conclusion. Likewise, counting corners differently changes the problem instead of revealing a compromise within the original guarantee.

There can be tensions in representing a real map or in presenting and checking a proof. Those belong to the modeling or evidential task. The proof and specification methods described above explain how the theorem is established and expressed; they do not add opposed objectives to its identity. The distinction preserves the exact guarantee without turning its hypotheses, boundaries or history into artificial trade-offs.

Structural–Framed Character¶

The theorem is strongly structural within mathematics. Its truth concerns a graph class, a label set and a quantified relation between them. The statement does not rank one pigment, vertex or human purpose above another.

Evaluative weight. A proper coloring meets explicit edge inequalities. Four is a proved bound, not an aesthetic recommendation or a claim that four labels are desirable in every application.

Human-practice dependence. People choose which real objects become vertices and which contacts become edges. Those modeling choices affect whether the theorem is applicable. Once the graph and definitions are fixed, the existence of a proper assignment does not depend on those preferences.

Institutional origin. Publication, independent checking and formal verification provide grounds for accepting the proof. They do not constitute the adjacency relation or make a monochromatic edge proper by agreement. The mathematical statement remains distinct from the institutions that communicate it.

Vocabulary travel. Vertices, edges and labels support literal translations among the demonstrated graph, map and tetrahedral-face representations. The exact four-color guarantee travels with its premises; renaming labels as resources does not establish those premises in an arbitrary new setting.

Import versus recognition. Applying the theorem requires recognizing the finite loopless planar graph relation. Merely calling a complicated allocation a four-color problem supplies no missing planarity proof and removes none of its extra constraints.

Its character: strongly structural and mathematically domain-bound; a precise graph class supports a universal labeling guarantee, while the choice of how to represent an external map determines whether that relation has actually been instantiated.

Structural Core vs. Domain Accent¶

The portable core is conflict-free assignment under pairwise separation constraints, represented by the catalog's Graph Coloring Prime. Its variables are items, conflict pairs, palette labels and an assignment that honors the conflicts. That pattern can be reused without preserving any particular map shape or physical interpretation of a color.

The Four Color Theorem adds indispensable mathematical commitments: finite loopless undirected graphs, a planar embedding premise, vertex rather than edge labeling, one common palette and a universal bound of four. Dropping those commitments leaves a more general coloring problem but loses this exact guarantee. They are part of the result's identity, rather than optional decoration around a substrate-neutral rule.

The named theorem therefore remains a domain-specific mathematical abstraction. Its graphical representations can change literally while the same structure is retained. Broader claims about fair allocation, uniform access or “four resources always suffice” would require their own identity and evidence; renaming the theorem's terms does not establish them.

This entry is part of Graph Coloring and is a kind of Formal theorem.

Graph Coloring supplies the related general pattern: assign labels so that conflicting pairs differ. The Four Color Theorem guarantees that some such assignment exists within a particular palette for a particular graph class. A theorem about those assignments and an individual coloring operation answer different questions.

Computer-Assisted Proof concerns a way of establishing a result. The inspected RSST manuscript uses computer-supported reducibility and unavoidability analysis; Gonthier's published account discusses formal proof and the bridge to the intended map specification. Those methods explain the warrant for the result without replacing its mathematical statement.^[1]^[2]

Graph Duality is a neighboring representation construction. In suitable planar embeddings, a face-coloring question can be expressed through vertex adjacency. The explicit map and tetrahedron translations above use that relationship without making a second theorem or counting the same graph twice. Planarity names the premise being used, and Chromatic Number names the individual-graph quantity being bounded.

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

Show alternative path (1)

Neighborhood in Abstraction Space¶

Four Color Theorem sits in a moderately populated region (54^th 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

Not to Be Confused With¶

Graph Coloring: the general assignment relation or problem. Ask whether the claim concerns finding a coloring of a particular conflict graph or a universal theorem for the planar class.
Chromatic Number: the smallest palette needed by one graph. The theorem bounds that quantity by four for its class; the two worked cases have different minima.
Planarity: existence of a crossing-free embedding. A coloring does not certify this. For example, $K_{3,3}$ has a two-coloring by its two vertex parts. If it were planar, Euler's formula and face lengths of at least four would give $e\leq2v-4=8$, contradicting its nine edges on six vertices. This elementary counterexample shows why the implication cannot be reversed.
Edge coloring: labels go on edges, with incident-edge conflicts, rather than on the vertices of the original graph.
List coloring: each vertex has its own allowed list. A theorem using one common four-element palette does not automatically settle independently specified lists.
Greedy coloring: an assignment procedure governed by a vertex order and local choices. The existence of a four-coloring does not promise that every such procedure or order finds one.
Graph Duality: a representation translation between embedded vertices and faces. Translating a theorem's instance is different from proving its uniform bound.
Computer-Assisted Proof: an evidential method whose inputs and correctness bridge need their own analysis. Neither a successful example nor the presence of a computer substitutes for a proof of the quantified theorem.

References¶

[1] 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. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j ↩k

[2] 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. registry ↩a ↩b ↩c ↩d ↩e ↩f ↩g ↩h ↩i ↩j