The two pillars of the proof: reducible configurations and the discharging method
Two ideas finish the proof: some small patterns can always be colored around, and every planar graph is forced to contain one of them.
Use Previous and Next to browse four reducible configurations, and press Play Animation to watch a coloring of the outer ring extend to the vertices inside.
A vertex of degree 4 surrounded by its ring of 4 neighbors. If the ring uses at most 3 of the 4 colors, the leftover color works for the center. If all 4 colors appear, a Kempe chain argument saves us: either the chain between two opposite ring vertices fails to connect them (swap it), or it separates the other two ring vertices (swap their chain instead). Either way a color is freed for the center.
Ring vertices start pre-colored. Click "Play Animation" to watch the inner vertices get colored one by one, extending the ring coloring inward. Use Previous/Next to browse different reducible configurations.
The proof of the four color theorem rests on two pillars -- reducibility and discharging. A configuration is reducible if any valid 4-coloring of its surrounding ring of vertices can be extended to include the interior vertices. The discharging method proves that an unavoidable set of reducible configurations must appear in every planar graph.
Together, these two ideas complete the proof: since every planar graph must contain at least one configuration from the unavoidable set, and every such configuration is reducible, any minimal counterexample to the four color theorem leads to a contradiction. There can be no smallest non-4-colorable planar graph.
A configuration is a small subgraph together with its surrounding ring of vertices.
Key insight: A configuration is reducible when every possible coloring of the ring of vertices surrounding it can be extended to a valid 4-coloring of the interior. If we know every graph contains a reducible configuration, we can always make progress in a coloring proof.
A configuration is reducible if ring colorings always extend inward -- it can be "conquered" in any coloring proof by handling the ring first and then filling in the interior.
Every vertex starts with charge 6 minus its degree. Apply Rule 1 and Rule 2 and watch charge move between vertices while the total stays fixed -- then see where positive charge is left.
Each vertex starts with charge 6 - degree. Blue = positive charge, red = negative, gray = zero. Apply discharging rules to redistribute charge. The total charge equals 6V - 2E, which Euler's formula makes at least 12 for any planar graph (exactly 12 for triangulations), so positive charge must exist somewhere, forcing certain low-degree configurations to appear.
Discharging assigns each vertex an initial charge of 6 - degree. The total charge is 6V - 2E, which by Euler's formula is always positive for a planar graph -- at least 12, and exactly 12 for a triangulation. Discharging rules redistribute charge between vertices without changing the total -- and by analyzing where positive charge ends up, we can prove that certain configurations must appear.
Key insight: Discharging assigns charges based on vertex degree and redistributes them. By Euler's formula, the total charge is always at least 12. Since positive charge must exist somewhere, the discharging rules force certain structures to appear.
Press Try Another Graph and see which configuration from the set turns up each time. No planar graph escapes all of them.
Graph 1 of 6
Found: Vertex of degree 4 or less
Vertex 0 has degree 3. Any planar graph must contain a vertex of degree at most 5 -- and here we found one with degree 3 or less, which is even more constrained.
Every planar graph must contain at least one of these configurations. The highlighted vertices and edges show the detected configuration. Click "Try Another Graph" to see different examples -- in each one, at least one configuration from the unavoidable set is always present.
An unavoidable set is a collection of configurations such that every planar graph must contain at least one member. The discharging method is the tool used to prove unavoidability.
Key insight: An unavoidable set is a collection of configurations such that every planar graph contains at least one. If every configuration in an unavoidable set is also reducible, the four color theorem follows.
The four color theorem follows from finding an unavoidable set where every member is reducible -- this is exactly what Appel and Haken accomplished (with 1,936 configurations checked by computer).
Spot a mistake or have an idea?