O teorema das quatro cores afirma que qualquer mapa desenhado num plano pode ser colorido com no máximo quatro cores, de modo que duas regiões que partilhem uma fronteira não tenham a mesma cor. Duas regiões que apenas se tocam num único ponto podem partilhar cor. O teorema aplica-se a qualquer mapa, por mais complexo que seja.
As regiões 1, 2, 3 e 4 fazem fronteira com várias outras. As regiões da esquerda (4) e da direita (4) não partilham fronteira, por isso podem ter a mesma cor. Aqui são necessárias exatamente 4 cores.
Francis Guthrie formulou a conjetura em 1852 enquanto coloria um mapa dos condados ingleses. Reparou que quatro cores pareciam sempre suficientes, mas não conseguiu prová-lo. O problema derrotou matemáticos durante 124 anos. Muitas falsas provas foram publicadas e refutadas. Cinco cores são sempre suficientes e isso pode ser provado à mão usando a fórmula de Euler para grafos planares.
O teorema das quatro cores levou 124 anos desde a conjetura até à prova. A prova de 1976 foi o primeiro grande teorema verificado por computador.
A prova de 1976 de Kenneth Appel e Wolfgang Haken foi o primeiro grande teorema provado com ajuda de computador. Reduziu todos os mapas possíveis a 1.936 configurações e fez um computador verificar cada uma durante mais de 1.200 horas de CPU. Muitos matemáticos sentiram desconforto com uma prova que não podia ser verificada à mão. Uma prova legível por humanos, se existir, continua por descobrir.
Cinco regiões exteriores (um número ímpar) obrigam o anel a usar 3 cores: não existe 2-coloração de um ciclo de 5. A região central é adjacente às cinco, toca nas três cores do anel e por isso precisa de uma quarta cor. Isto mostra que quatro cores são por vezes realmente necessárias.
Todo o mapa desenhado num plano pode ser colorido com no máximo quatro cores, de modo que duas regiões que partilham uma fronteira não tenham a mesma cor. A conjetura foi formulada por Francis Guthrie em 1852. Foi provada por Appel e Haken em 1976 usando um computador para verificar 1.936 configurações, tornando-se o primeiro grande teorema provado com assistência computacional. Uma verificação mais curta de Robertson, Sanders, Seymour e Thomas, em 1997, reduziu esse número para 633 configurações. O teorema não vale num toro, onde podem ser necessárias sete cores.