Slaying the Kraken:

Abstract

This paper outlines the history of the four-colour conjecture (that four colours suffice to colour in any map drawn on a plane in such a way that no countries that share a border are the same colour). It describes the conjecture's origins, the first claimed proof (in 1879), the refutation of that proof (in 1890), and the developments that led to Kenneth Appel and Wolfgang Haken's celebrated, computer-assisted solution of the problem in 1976. There is a brief discussion of the significance of the new computerized proof by Robertson, Sanders, Seymour and Thomas. The paper describes fierce controversy over whether or not the Appel-Haken solution should be regarded as a `proof', and contrasts the case of the four-colour theorem with Imre Lakatos' history of the proof of Euler's polyhedral formula. While Lakatos showed the negotiation of concepts such as `polyhedron', `face' and `edge', the history of the four-colour theorem reveals the negotiability of `proof' itself, and therefore of the boundary of what constitutes mathematical knowledge.