The Four Color Theorem

Reduction to a minimal counterexample. If the theorem were false, take a planar graph requiring 5 or more colors with the fewest possible vertices. Adding edges to a planar graph while keeping it planar can only increase the number of colors needed, so this minimal counterexample can be assumed to be a maximal planar graph (a triangulation), where every face, including the outer one, is bounded by exactly 3 edges.

Discharging setup. Assign to every vertex $v$ an initial charge $6 - \deg(v)$. Using $V - E + F = 2$ together with $2E = \sum_v \deg(v)$ and $3F \le 2E$ (each face has at least 3 sides), the total charge over all vertices works out to exactly $12$, hence strictly positive. The discharging method then moves charge locally between nearby vertices according to a fixed set of rules, without changing this total; analyzing where positive charge must remain after redistribution shows that some vertex of low degree, together with a specific pattern of neighbors, must occur somewhere in the graph. These finitely many patterns are called the unavoidable configurations, since at least one of them is present in every planar triangulation.

Reducibility. A configuration is called reducible if, whenever it appears inside a hypothetical minimal counterexample, any 4-coloring of the smaller graph obtained by removing or contracting that configuration can always be re-extended to a 4-coloring of the whole graph, contradicting minimality. Appel and Haken (1976) verified computationally that every configuration in their unavoidable list of 1,936 configurations (later trimmed to 633 by Robertson, Sanders, Seymour and Thomas in 1997) is reducible, using well over a thousand hours of computer time. This made the Four Color Theorem the first major theorem whose proof relied essentially on machine computation, later independently re-verified and, in 2005, formally checked line by line inside the Coq proof assistant by Gonthier.

Conclusion. Since every unavoidable configuration is reducible, no minimal counterexample can exist: no planar graph needs 5 or more colors, so $\chi(G) \le 4$ for every planar graph $G$.