Lesson 2

The conjecture was stated in 1852 by Francis Guthrie. The first proof was given by Kenneth Appel and Wolfgang Haken in 1976, with the detailed write-up appearing in 1977. Their argument reduced the theorem to checking many reducible configurations, and that checking was done by computer. This is why the four-color theorem became so famous: it was the first major theorem whose proof essentially relied on computation.

A later proof by Robertson, Sanders, Seymour, and Thomas made the argument substantially cleaner and reduced the computer part to checking 633 configurations. However, this proof still relies on computer verification, so a purely hand-checkable proof is still not known.

In 2005, Georges Gonthier and Benjamin Werner gave a formally verified proof in the Coq proof assistant. This increased confidence in the result, but it is still a computer-assisted proof rather than a traditional proof that can be checked entirely by hand.