Computer-Assisted Proofs of the Four Color Theorem

From a Global Coloring Problem to Finite Checks

The Four Color Theorem says that every planar graph has a proper vertex coloring with at most four colors. A proper coloring assigns colors to vertices so that the endpoints of every edge have different colors. The theorem is simple to state, but its proof required a long chain of structural arguments followed by extensive computation. Appel and Haken’s proof, announced in 1976 and published with Koch in 1977, was the first major theorem whose proof relied on a computer for a large finite verification.

The strategy is not to ask a computer to color every planar graph. There are infinitely many planar graphs. Instead, the proof reduces the problem to a finite collection of local patterns in plane triangulations. Two properties do the essential work: every triangulation must contain at least one pattern from a designated collection, and each pattern in that collection must be reducible. The earlier material on unavoidable sets and reducible configurations develops these ideas; here we focus on how a computer can check the finite part and how that checking fits into the proof.

For a basic form of reducibility, regard a configuration as a patch with a boundary cycle. Remove the interior of the patch, color the remaining graph, and ask whether every proper coloring of the boundary extends to the patch. If it does, the configuration cannot occur in a minimal counterexample: a coloring of the smaller graph would extend to a coloring of the counterexample. Some reducibility tests in full proofs require more elaborate reductions than this simple extension test, but the logical purpose is the same.

The Logical Structure of the Proof

It suffices to consider plane triangulations: a planar graph with at least three vertices can be extended, by adding edges in its faces when needed, to a plane triangulation on the same vertex set, and a coloring of the triangulation restricts to a coloring of the original graph. The cases with fewer than three vertices can be colored directly. Suppose, for contradiction, that some plane triangulation has no proper four-coloring. Choose one with the fewest vertices. It is a minimal counterexample.

Proof. Assume that the Four Color Theorem is false, and choose a plane triangulation \(G\) with the fewest vertices among all counterexamples. By unavoidability, \(G\) contains an occurrence of some configuration \(C\) in the family. Since \(C\) is reducible, its occurrence is forbidden in a minimal counterexample. This contradicts the choice of \(G\). Therefore no counterexample exists, and every planar graph has a proper four-coloring. \(\square\)

This principle separates two kinds of reasoning. The unavoidable-set argument is a global structural argument: it proves that some member of a finite family must appear. Reducibility is a local argument: it rules out each member in a minimal counterexample. Computer assistance enters principally in checking many detailed local cases; it does not replace the proof that the family is unavoidable.

What a Computer Checks

A finite reducibility check can be phrased as an exhaustive search. For a patch with boundary vertices \(b_1,\dots,b_k\), list the boundary color assignments that are proper on boundary edges. For each assignment, test whether the interior vertices can be colored so that all patch edges have differently colored endpoints. The colors are taken from \(\{1,2,3,4\}\). An assignment that gives the same color to the endpoints of a boundary edge is not a proper boundary coloring and is excluded.

Proof. Suppose the patch occurs in a minimal counterexample \(G\). Delete its interior vertices, retaining the rest of \(G\) and the boundary. The resulting graph is planar and has fewer vertices than \(G\). By the minimality of \(G\), it has a proper four-coloring. The colors on the boundary form a proper boundary coloring, since every boundary edge is retained. By the hypothesis, this boundary coloring extends over the deleted patch. Combining the coloring outside the patch with the extension inside gives a proper four-coloring of \(G\), contradicting that \(G\) is a counterexample. Thus the patch cannot occur in a minimal counterexample. \(\square\)

Worked Checks on Small Patches

Appel–Haken and Later Refinements

The Appel–Haken proof used a large finite unavoidable set and computer-checked reducibility calculations. The original unavoidable set is commonly described as containing 1,936 configurations. The size and complexity of the verification made the proof difficult to audit by hand, but the underlying logic remained a conventional mathematical implication: establish unavoidability, verify reducibility, and apply the minimal-counterexample argument.

A later proof by Robertson, Sanders, Seymour and Thomas, published in 1997, refined the strategy and used a smaller unavoidable set, commonly reported as 633 configurations. The reduction in size and the organization of the verification made the proof more manageable; it did not turn the theorem into a short hand calculation. Later formal verification work, notably Gonthier’s proof in the Coq proof assistant, encoded the mathematics so that a proof-checking system could verify the resulting formal proof.

These developments address different concerns. A computer program that exhaustively checks cases can make a large finite proof feasible, but confidence also depends on the correctness of the encoding, the program and the execution. A formal proof assistant checks a proof expressed in a formal language against its rules of inference. Formalization improves the audit trail, but it still relies on the mathematical definitions and on correctly connecting the formal statement to the theorem intended.

What the Computation Does—and Does Not—Establish

The computation verifies finite claims specified by the proof. Depending on the implementation, these can include that a listed boundary coloring has an extension, that an alleged obstruction really blocks all extensions, or that a finite collection of local cases has been exhausted. A search is conclusive only when its case-generation rules cover every allowed case and its tests implement the stated mathematical condition.

The computation alone does not establish that every triangulation contains a member of the list. That is the separate unavoidability argument. Nor does a list of successful local colorings prove the Four Color Theorem unless the local extension property really excludes the configurations from a minimal counterexample. The global proof depends on the links between these claims, not just on the number of computations performed.

Common pitfall. It is incorrect to say, “The computer checked some configurations, so it proved every planar graph is four-colorable.” A finite check proves only the specific finite statements encoded in it. The correction is to identify the full chain: the graph can be reduced to a minimal triangulation counterexample; that triangulation must contain a listed configuration; each listed configuration is excluded by its checked reducibility argument; hence no minimal counterexample exists. Omitting the unavoidability step leaves a gap.

The importance of the computer-assisted proof is therefore methodological as well as historical. It shows how a theorem about an unbounded class of graphs can be proved by combining a global structural argument with carefully specified finite verification. The essential standard is not that a machine produces an answer, but that the answer is attached to a complete mathematical argument whose assumptions, cases and logical consequences can be examined.