Dado um mapa plano, dividido em regiões,  quatro cores chegam para o colorir, de forma a que regiões vizinhas não partilhem a mesma cor. 

     (Nota: Regiões que só se tocam num ponto não são consideradas vizinhas.)
 
 

          Este teorema foi demonstrado com a ajuda de um computador IBM360 em 1976 por Appel (matemático americano) e Haken (matemático alemão). A prova mostrava que, se para cerca de 2000 formas “básicas” de mapas era possível colorir as regiões nas condições do teorema, então para qualquer outro mapa também seria.

Sendo a prova actual demasiado longa, as verificações a fazer não podem ser feitas directamente por um ser humano. Trata-se do primeiro grande resultado, cuja prova exigiu o recurso a meios informáticos.

Em Abril de 1975, Martin Gardner apresentou um mapa, com 110 regiões e dizia que, para aquele exemplo, seriam necessárias cinco cores. Seria assim um contra-exemplo, colocando em dúvida o Teorema das Quatro Cores. Este acto não passou de uma brincadeira realizada no "Dia das Mentiras". Realmente era difícil utilizar apenas quatro cores, mas não era impossível.

Tente também colorir este pretenso contra-exemplo de Martin Gardner.

Em 1994, uma prova simplificada, da autoria dos matemáticos americanos Paul Seymour, Neil Robertson, Daniel Sanders e Robin Thomas foi anunciada, reduzindo a 633 os casos a verificar e utilizando algoritmos mais eficientes. O uso do computador continua indispensável.
 
 

Realmente, este é um problema que qualquer pessoa, sem preparação matemática, pode entender e no entanto a demonstração actualmente conhecida é bastante elaborada.