In 1890, Heawood pointed out that Kempe’s argument was wrong. However, in that paper he proved the five color theorem, saying that every planar map can be colored with no more than "five" colors, using ideas of Kempe. In the following century, a vast amount of work and theories were developed to reduce the number of colors to four, until the four color theorem was finally proved in 1976 by Kenneth Appel and Wolfgang Haken. The proof went back to the ideas of Heawood and Kempe and largely disregarded the intervening developments. The proof of the four color theorem is also noteworthy for being the first major computer-aided proof.