Four Color Theorem

Four Color Theorem. The Four Color Theorem is a foundational result in graph theory and topology, stating that any map drawn on a plane or a sphere can be colored using at most four colors such that no two adjacent regions share the same color. First conjectured in the mid-19th century, it resisted proof for over a century, becoming one of the most famous problems in mathematics. Its eventual proof in 1976 by Kenneth Appel and Wolfgang Haken was groundbreaking for its extensive use of computer assistance, sparking lasting debates about the nature of mathematical proof.

Statement of the theorem

The theorem asserts that the regions of any planar graph can be assigned one of four colors, with the constraint that any two regions sharing a common boundary segment of non-zero length receive different colors. This formulation translates the cartographic problem into the language of combinatorics. The theorem holds equivalently for maps on the surface of a sphere, as established through stereographic projection. It is a statement about chromatic number and is deeply connected to the properties of Euler characteristic for planar subdivisions.

Historical background

The problem originated in 1852 when Francis Guthrie, while coloring a map of the Counties of England, conjectured that four colors sufficed. He communicated it to his brother Frederick Guthrie, who in turn mentioned it to their professor, the renowned Augustus De Morgan of University College London. De Morgan discussed the problem in correspondence with William Rowan Hamilton, but no significant progress was made. In 1879, Alfred Kempe, a barrister and mathematician, published a proof in the American Journal of Mathematics that was accepted for a decade. Its flaw was exposed in 1890 by Percy Heawood, who also proved the Five Color Theorem. The quest for a proof attracted attention from figures like Arthur Cayley and became a major unsolved challenge, listed by David Hilbert among important problems for the 20th century.

Proof

The first correct proof was announced in 1976 by mathematicians Kenneth Appel and Wolfgang Haken at the University of Illinois Urbana-Champaign. Their method relied on reducibility and discharging, two techniques developed from earlier work by Heinrich Heesch. They constructed an unavoidable set of 1,936 configurations and used a computer program to demonstrate that each was reducible, meaning it could not appear in a minimal counterexample. This required over a thousand hours of computation on IBM systems. The proof was controversial because of its computer-assisted nature, challenging traditional notions of mathematical proof as verifiable by hand. Its correctness was later verified using different software and approaches, including work by Neil Robertson and Paul Seymour.

Generalizations and related problems

Generalizations consider coloring maps on surfaces of higher genus; for a torus, the Heawood conjecture (proved by Gerhard Ringel and J. W. T. Youngs) gives a formula. The related Hadwiger conjecture in graph theory is a major open problem. The question of list coloring and edge coloring for planar graphs also stems from this theorem. Research into algebraic graph theory and topological graph theory has been heavily influenced by these inquiries. The search for a concise, human-surveyable proof remains an active area, pursued by mathematicians like Georges Gonthier who used the Coq proof assistant for formal verification.

Applications

While its primary application was to theoretical cartography, the theorem's real impact is in the development of algorithms and fields like computer science. It underpins algorithms for register allocation in compiler design, where a limited number of processor registers must be assigned to program variables. The methodologies from its proof advanced the field of automated theorem proving and computational mathematics. Concepts of graph coloring are applied in scheduling problems, frequency assignment for mobile networks, and sudoku puzzle design. The theorem also serves as a classic pedagogical tool in courses on discrete mathematics and combinatorial optimization.

Category:Graph theory Category:Theorems in discrete mathematics Category:1976 in science