Teorema Das Quatro Cores

Adjacente significa que duas regiões compartilham um segmento de curva limite comum, não apenas um canto onde três ou mais regiões se encontram. Foi o primeiro teorema importante a ser provado usando um computador. Inicialmente, essa prova não foi aceita por todos os matemáticos porque a prova assistida por computador era inviável para um ser humano verificar manualmente. Desde então, a prova ganhou ampla aceitação, embora alguns questionadores permaneçam.

A sua formulação é a seguinte:

Dado um mapa plano, dividido em regiões, quatro cores são suficientes para colori-lo de forma a que regiões vizinhas não partilhem a mesma cor.

O teorema das quatro cores foi provado em 1976 por Kenneth Appel e Wolfgang Haken após muitas provas e contra-exemplos falsos (ao contrário do teorema das cinco cores, provado na década de 1800, que afirma que cinco cores são suficientes para colorir um mapa). Para dissipar quaisquer dúvidas remanescentes sobre a prova Appel-Haken, uma prova mais simples usando as mesmas ideias e ainda contando com computadores foi publicada em 1997 por Robertson, Sanders, Seymour e Thomas. Além disso, em 2005, o teorema foi provado por Georges Gonthier com software de prova de teorema de uso geral.

Dror Bar-Natan deu uma demonstração sobre Álgebra de Lie e Invariante de Vassiliev que é equivalente ao teorema das quatro cores.[25]

Apesar da motivação de colorir mapas políticos de países, o teorema não é de interesse particular para os cartógrafos. De acordo com um artigo do historiador de matemática Kenneth May, "Mapas que utilizam apenas quatro cores são raros, pois geralmente requerem apenas três. Livros sobre cartografia e história da cartografia não mencionam a propriedade de quatro cores" (Wilson 2014, 2). O teorema também não garante a exigência cartográfica usual de que regiões não contíguas de um mesmo país (como o exclave do Alasca e o resto dos Estados Unidos) sejam coloridas de forma idêntica.