Four color theorem

Every planar map can be colored with at most four colors so that regions sharing a boundary segment have different colors. Equivalently, every planar graph has chromatic number at most four.

Planar graph: A graph that can be drawn in the plane without edges crossing except at shared endpoints. Map regions become vertices, and shared boundary segments become edges.
Francis Guthrie: A British mathematician who posed the map-coloring problem in 1852. His question about coloring English counties initiated the problem.
Map graph: A graph whose vertices represent map regions and whose edges represent shared boundary segments. This construction expresses map coloring as a graph-coloring problem.
Five color theorem: Every planar graph has a proper vertex coloring with at most five colors. It has a comparatively short proof, unlike the four-color theorem's extensive case analysis.
Computer-assisted proof: A mathematical proof whose verification depends on calculations performed by a computer. The theorem's proof made extensive computation part of an accepted mathematical argument.
Graph coloring: An assignment of labels to graph vertices in which adjacent vertices receive different labels. The theorem is a universal upper bound on the number of colors needed.
Augustus De Morgan: A British mathematician who circulated Francis Guthrie's map-coloring question in 1852. Guthrie's question reached the mathematical community through De Morgan.
Vertex coloring: A graph coloring that assigns colors to vertices so adjacent vertices have different colors. The theorem concerns vertex coloring after regions are represented by vertices.
Four color theorem for maps: The map-coloring formulation requiring different colors only for regions that share a boundary segment. This formulation clarifies why regions meeting only at a point need not have different colors.
Four-color theorem formalization: A machine-checked proof of the four color theorem encoded in a formal logical system. Formalization addressed concerns about verifying the computer's role in the original proof.

Linked from 15 pages