El teorema de los cuatro colores establece que cualquier mapa dibujado en un plano se puede colorear con un máximo de cuatro colores de modo que dos regiones que comparten frontera nunca tengan el mismo color. Dos regiones que solo se tocan en un único punto pueden compartir color. El teorema se aplica a cualquier mapa, sin importar su complejidad.
Las regiones 1, 2, 3, 4 limitan cada una con varias otras. Las regiones izquierda (4) y derecha (4) no comparten frontera, así que pueden compartir color. Aquí se necesitan exactamente 4 colores.
Francis Guthrie conjeturó el teorema en 1852 mientras coloreaba un mapa de los condados ingleses. Notó que cuatro colores siempre parecían suficientes, pero no pudo demostrarlo. El problema desconcertó a los matemáticos durante 124 años. Se publicaron y refutaron muchas demostraciones falsas. Cinco colores siempre bastan, y esto se puede demostrar a mano usando la fórmula de Euler para grafos planos.
El teorema de los cuatro colores tardó 124 años desde la conjetura hasta la demostración. La demostración de 1976 fue el primer gran teorema verificado por ordenador.
La demostración de 1976 de Kenneth Appel y Wolfgang Haken fue el primer gran teorema demostrado por ordenador. Redujo todos los mapas posibles a 1.936 configuraciones e hizo que un ordenador verificara cada una durante más de 1.200 horas de tiempo de CPU. Muchos matemáticos se sentían incómodos con una demostración que no podía verificarse a mano. Una demostración legible por humanos, si existe, aún no se ha descubierto.
Cinco regiones exteriores (un número impar) obligan al anillo a usar 3 colores: no existe una 2-coloración de un 5-ciclo. La región central es adyacente a las cinco, tocando los tres colores del anillo, por lo que necesita un cuarto color. Esto demuestra que cuatro colores son realmente necesarios a veces.
Todo mapa dibujado en un plano se puede colorear con un máximo de cuatro colores de modo que dos regiones que comparten frontera nunca tengan el mismo color. Conjeturado por Francis Guthrie en 1852. Demostrado por Appel y Haken en 1976 usando un ordenador para verificar 1.936 configuraciones, convirtiéndose en el primer gran teorema demostrado con asistencia informática. Una verificación más breve de Robertson, Sanders, Seymour y Thomas en 1997 redujo esto a 633 configuraciones. El teorema no se cumple en un toro, donde pueden requerirse siete colores.