Four Color Reduction and the Computer

Frank Bernhart

Rochester, New York

Abstract

The Four Color Conjecture for maps has a dual form: the vertices of every 5-connected (finite) planar triangulation T can be 4-colored. The simplest case is the skeleton of the icosahedron, the planar dual of the dodecahedron map.

The interior C of a small circuit or ”ring” is reducible if a procedure developed by G.D. Birkhoff in 1913 succeeds in coloring T by modifying C. The classical approach is to construct a set/list U of reducible configurations and show also that every triangulation T contains at least one member of U (unavoidable).

For fifty years, the manual computation of reducibility gradually increased the number N such that all T with at most N vertices can be four colored. The final solution of Appel and Haken raised N to infinity (from 96), aided by computer reduction. Thousands of hours of human-machine cooperation were needed. Though the proof at some levels is satisfying, the details are horrendous.

As the Four Color Theorem nears its twentieth birthday, interest in checking or revising the proof is rebuilding. A few advances in theory may perhaps shorten the labor. Is the time ripe for a team of mathematically minded programmers to work out a plan ?