Page "Four color theorem" Paragraph 5

The four color theorem was proven in 1976 by Kenneth Appel and Wolfgang Haken.

It was the first major theorem to be proved using a computer.

Appel and Haken's approach started by showing that there is a particular set of 1, 936 maps, each of which cannot be part of a smallest-sized counterexample to the four color theorem.

Appel and Haken used a special-purpose computer program to confirm that each of these maps had this property.

Additionally, any map ( regardless of whether it is a counterexample or not ) must have a portion that looks like one of these 1, 936 maps.

Showing this required hundreds of pages of hand analysis.

Appel and Haken concluded that no smallest counterexamples existed because any must contain, yet not contain, one of these 1, 936 maps.

This contradiction means there are no counterexamples at all and that the theorem is therefore true.

Initially, their proof was not accepted by all mathematicians because the computer-assisted proof was infeasible for a human to check by hand.

Since then the proof has gained wider acceptance, although doubts remain.