Four color theorem (computer-assisted proof)
Teorema de los cuatro colores (primera prueba asistida por ordenador)
- Date
- 1976 · confidence high
- Place
- Urbana, Illinois, United States
- Credited to
- Kenneth Appel and Wolfgang Haken (conjecture by Francis Guthrie, 1852)
- People
- 👤 Kenneth Appel1932–2013👤 Wolfgang Haken1928–2022
- Field
- Knowledge & symbols
What was discovered
Every planar map can be coloured with four colours so that no two neighbouring regions share a colour. The proof checked 1,936 unavoidable configurations with more than a thousand hours of computer time, which opened the debate on what counts as a proof.
Robertson, Sanders, Seymour and Thomas simplified the proof in 1996; Gonthier fully verified it in Coq in 2005.
What it led to
- computer-assisted proofs
- structural graph theory
- formal verification (Coq proof by Gonthier, 2005)
Built on
- Euler formula and Euler identity1748
- five colour theorem (Heawood, 1890)
- Kempe (flawed proof, 1879)
Made possible
- Proof of the Kepler conjecture1998 (verificación formal 2014)
- frequency and register allocation (graph colouring)