Appel-Haken 1976, the proof controversy, and modern verification
In 1976 Kenneth Appel and Wolfgang Haken announced they had proved the four color theorem -- with the help of a computer. The mathematical community was stunned: it was the first major theorem whose proof relied essentially on computation. No human could check the entire argument by hand, and many mathematicians questioned whether it was truly a "proof" at all.
Half a century later, the proof has been independently verified three times with increasing rigor. The debate it sparked about the nature of proof continues to shape how mathematicians think about certainty, computation, and understanding.
The proof works by contradiction. Assume a minimal counterexample exists -- the smallest planar graph that cannot be 4-colored. Walk through the flowchart below to see how the argument unfolds step by step, from the initial assumption to the final contradiction.
Click each node to expand its explanation. Nodes you have visited will be fully highlighted.
0 of 6 steps explored.
Key insight: The proof works by contradiction. Assume a minimal counterexample exists. By discharging, it must contain one of 1,936 configurations. But each one is reducible (verified by computer), so the counterexample can be made smaller -- contradicting minimality.
For each of the 1,936 configurations, the computer verified that every possible coloring of the surrounding ring of vertices extends to a valid 4-coloring of the interior. Select a simplified configuration below and watch the verification process in action.
Select a configuration and run the verification. The computer checks that every valid coloring of the ring boundary can be extended to a proper 4-coloring of the entire configuration, proving it is reducible.
Key insight: For each of the 1,936 configurations, the computer verified that every possible coloring of the surrounding ring extends to the interior. This is a finite but enormous case analysis -- far beyond what any human could check by hand.
The four color theorem has been proved three times, each with greater rigor and transparency. Compare the approaches below, from the controversial 1976 original to the formally verified 2005 formalization in the Coq proof assistant.
Kenneth Appel & Wolfgang Haken
The original proof was announced in 1976 after four years of work. Appel and Haken used a combination of hand-derived discharging rules and computer verification of 1,936 reducible configurations. The computer ran for approximately 1,200 hours on an IBM 370 mainframe. The proof was met with significant skepticism: the computer code was not publicly available, the output could not be checked by hand, and some mathematicians questioned whether it constituted a "real" proof.
Key insight: The proof has been independently verified three times with increasing rigor. Gonthier's 2005 Coq formalization reduced the trust assumption to the correctness of the Coq kernel -- a much smaller and well-tested piece of software.