Teorema de los cuatro colores (primera prueba asistida por ordenador)
Four color theorem (computer-assisted proof)
- Fecha
- 1976 · fiabilidad alta
- Lugar
- Urbana, Illinois, EE. UU.
- Autoría
- Kenneth Appel y Wolfgang Haken (conjetura de Francis Guthrie, 1852)
- Personas
- 👤 Kenneth Appel1932–2013👤 Wolfgang Haken1928–2022
- Ámbito
- Saber y símbolos
Qué se descubrió
Todo mapa plano puede colorearse con cuatro colores sin que regiones vecinas compartan color. La prueba comprobó 1936 configuraciones inevitables con más de mil horas de ordenador, lo que abrió el debate sobre qué es una demostración.
Robertson, Sanders, Seymour y Thomas simplificaron la prueba en 1996; Gonthier la verificó íntegramente en Coq en 2005.
A qué dio paso
- demostraciones asistidas por ordenador
- teoría de grafos estructural
- verificación formal (prueba en Coq por Gonthier, 2005)
Se apoya en
- Fórmula de Euler e identidad de Euler1748
- teorema de los cinco colores (Heawood, 1890)
- Kempe (prueba errónea, 1879)
Hizo posible
- Prueba de la conjetura de Kepler sobre empaquetamiento de esferas1998 (verificación formal 2014)
- asignación de frecuencias y registros (coloreado de grafos)