Appel-Haken 1976, the proof controversy, and modern verification
In 1976 a computer helped prove the four color theorem, and mathematicians argued over whether that counted as a proof at all.
Click each node in the flowchart, or press Walk Through All, to follow the argument from a smallest possible counterexample to a contradiction.
Click each node to expand its explanation. Nodes you have visited will be fully highlighted.
0 of 6 steps explored.
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.
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.
Pick a configuration and press Start Verification to watch every coloring of the outer ring get tested against the inside. Change the speed to see how fast the cases pile up.
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.
Switch between the three proofs to compare their configurations, methods, and trust levels. Open the discussion at the bottom to weigh both sides of the debate.
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.
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.
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.
Spot a mistake or have an idea?