# Four Colour Theorem

**Type:** Theorem  
**Domain:** Discrete Mathematics  
**Conjectured:** 1852, Francis Guthrie  
**Proved:** 1976, Kenneth Appel and Wolfgang Haken  
**Codex URL:** /mathematics/discrete/four-colour-theorem/  
**Entry status:** Live — v1.0 (2026-05-27)

## Statement
Any planar map can be coloured with 4 colours such that no two adjacent regions share a colour.

## Summary
First major theorem proved using essential computer assistance (1,936 cases checked, 1976). Formally verified in the Coq proof assistant by Gonthier, 2005.

## History
- Guthrie (1852): conjecture
- Kempe (1879): flawed proof, accepted 11 years
- Heawood (1890): found flaw; proved easier Five Colour Theorem
- Appel-Haken (1976): computer-assisted proof, 1,936 unavoidable configurations
- Robertson-Sanders-Seymour-Thomas (1997): simplified to 633 configurations
- Gonthier (2005): formal verification in Coq

## Philosophical debate
First proof requiring computer verification no human could check by hand — sparked debate (Tymoczko 1979) about the nature of mathematical proof.

## Sources
### Tier 1
- Appel, K. and Haken, W. (1977). Every planar map is four colorable. *Illinois J. Math.*, 21, 429-567.
- Robertson, N. et al. (1997). The four-colour theorem. *J. Combin. Theory B*, 70(1), 2-44.
### Tier 2
- Gonthier, G. (2008). Formal proof—the four-color theorem. *Notices of the AMS*.
### Tier 3
- Wilson, R. (2002). *Four Colors Suffice*. Princeton University Press.

---
*Mathematics Codex entry v1.0 — added 2026-05-27 — thecodex.expert/mathematics/*