Abstract:
The four colour theorem states that the vertices of every planar graph can be coloured with
at most four colours so that no two adjacent vertices receive the same colour. This theorem is
famous for many reasons, including the fact that its original 1977 proof includes a non-trivial
computer verification. Recently, a formal proof of the theorem was obtained with the equational
logic program Coq [14].
In this paper we describe an implementation of the computational method introduced in [7, 5]
to evaluate the complexity of the four colour theorem. Our method uses a Diophantine equational
representation of the theorem. We show that the four colour theorem is in the complexity class
CU,4. For comparison, the Riemann hypothesis is in CU,2 while Fermat’s last theorem is in class
CU,1.