---
tag: 0M406JC8J1
kind: statement
role: theorem
name: Four colour theorem
msc: [05C15, 05C10]
uses: [029JQEK15B, 0C5M7AM6FH]
sources:
  - url: https://en.wikipedia.org/wiki/Four_color_theorem
    locator: Formulation
same_as:
  wikidata: Q184410
  wikipedia: Four color theorem
---

## Statement

Let $G$ be a finite loopless [[planar graph|029JQEK15B]].
Then $\chi(G) \le 4$.

## Remarks

In terms of maps: four colours are enough for the regions of a map in the plane. Regions with a common boundary segment get different colours.
The bound is sharp, because $K_4$ is planar and $\chi(K_4) = 4$.

## History

Francis Guthrie stated the problem in 1852.
Kenneth Appel and Wolfgang Haken proved the theorem in 1976, with the help of a computer.
Robertson, Sanders, Seymour and Thomas gave a simpler proof in 1997. Georges Gonthier and Benjamin Werner checked a proof in the Coq proof assistant in 2005.

## Explanations

### L1 human

Four colours are enough to colour any map, so that neighbouring countries always have different colours.
It was the first major theorem whose proof needed a computer.