This theorem was conjectured in 1853 by [Francis Guthrie]? and finally proven in 1977 by [Ken Appel]? and [Wolfgang Haken]?. The proof reduced the infinitude of possible maps to 1476 configurations which had to be checked one by one by computer. The work was independetly double checked with different programs and computers.
The four color theorem was the first major theorem to be proven using a computer, and it was not accepted by all mathematicians because it could not directly be verified by a human. Ultimately, one had to have faith in the correctness of the compiler and hardware executing the program used for the proof.
To formally state the theorem, it is easiest to rephrase it in graph theory. It then states that the vertices of every planar graph can be colored with at most four colors so that no two adjacent vertices receive the same color. Or "every planar graph is four-colorable" for short.
![[Home]](wikipedia.png)