# zbMATH — the first resource for mathematics

The complexity of the four colour theorem. (English) Zbl 1235.03071
Summary: 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 [G. Gonthier, “Formal proof – the four color theorem”, Notices Am. Math. Soc. 55, No. 11, 1382–1393 (2008; Zbl 1195.05026)]. In this paper we describe an implementation of the computational method introduced by C. S. Calude and co-workers [C. S. Calude and E. Calude, “Evaluating the complexity of mathematical problems. I”, Complex Syst. 18, No. 3, 267–285 (2009; Zbl 1186.68226); C. S. Calude, E. Calude and M. J. Dinneen, “A new measure of the difficulty of problems”, J. Mult.-Val. Log. Soft Comput. 12, No. 3–4, 285–307 (2006; Zbl 1139.03028)] 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 $$\mathfrak C_{U,4}$$. For comparison, the Riemann hypothesis is in class $$\mathfrak C_{U,3}$$ while Fermat’s last theorem is in class $$\mathfrak C_{U,1}$$.

##### MSC:
 03D15 Complexity of computation (including implicit computational complexity) 05C15 Coloring of graphs and hypergraphs 05C85 Graph algorithms (graph-theoretic aspects) 11Y16 Number-theoretic algorithms; complexity
Coq
Full Text:
##### References:
 [1] Calude, Bull. EATCS 84 pp 167– (2004) [2] Calude, J. Mult. Valued Logic Soft Comput. 12 pp 285– (2006) [3] Calude, Complex Systems 18 pp 387– (2010) [4] Calude, Complex Systems 18 pp 267– (2009) [5] Wilson, Four colours suffice (2002) [6] Calude, Experiment. Math. 11 pp 369– (2002) · Zbl 1117.68385 · doi:10.1080/10586458.2002.10504481 [7] Calude, NZ Math. Magazine 38 pp 27– (2001) [8] Appel, Illinois J. Math. 21 pp 429– (1977) [9] Gonthier, Notices Amer. Math. Soc. 55 pp 1382– (2008) [10] Appel, Illinois J. Math. 21 pp 491– (1977) [11] Davis, Mathematical developments arising from Hilbert problems pp 323– (1976) · doi:10.1090/pspum/028.2/0432534 [12] Calude, Information and randomness: an algorithmic perspective (2002) · Zbl 1055.68058 · doi:10.1007/978-3-662-04978-5
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.