네 가지 색 정리는 평면 위에 그린 어떤 지도도, 경계를 공유하는 두 영역이 같은 색이 되지 않도록 네 가지 색만으로 색칠할 수 있다고 말한다. 놀랍게도 다섯 가지가 아니라 네 가지면 충분하며, 실제로 어떤 지도는 네 가지를 모두 필요로 한다.
어떤 평면 지도도 네 가지 색이면 충분하다. 네 색은 때때로 실제로 필요하며, 세 가지 색만으로는 항상 해결되지 않는다.
프랜시스 거스리는 1852년 영국의 주 지도를 색칠하다가 이 정리를 추측했다. 그는 네 가지 색이면 늘 충분해 보인다는 것을 알아차렸지만 증명하지는 못했다. 이 문제는 124년 동안 수학자들을 괴롭혔고, 많은 잘못된 증명이 발표되었다가 반박되었다. 다섯 가지 색이면 충분하다는 사실은 오일러의 평면그래프 공식을 이용해 손으로 증명할 수 있다.
네 가지 색 정리는 추측에서 증명까지 124년이 걸렸다. 1976년의 증명은 컴퓨터로 검증된 최초의 주요 정리였다.
1976년 케네스 애플과 볼프강 하켄의 증명은 컴퓨터를 이용해 증명된 최초의 주요 정리였다. 그들은 가능한 모든 지도를 1,936개의 구성으로 환원한 뒤, 컴퓨터로 각 구성을 1,200시간 이상 검증했다. 손으로 완전히 확인할 수 없는 증명이라는 점 때문에 많은 수학자들이 불편해했다. 사람이 읽을 수 있는 완전한 증명이 존재하는지는 아직도 알려져 있지 않다.
바깥의 다섯 영역(홀수 개)은 고리 부분만으로도 세 가지 색을 필요로 한다. 5-사이클은 두 색으로 칠할 수 없기 때문이다. 가운데 영역은 이 다섯 영역 모두와 인접하여 고리에서 쓰인 세 색을 모두 접하므로 네 번째 색이 필요하다. 그래서 어떤 경우에는 네 가지 색이 진짜로 필요하다.
평면에 그린 어떤 지도도 경계를 공유하는 두 영역이 같은 색이 되지 않도록 네 가지 색 이내로 칠할 수 있다. 프랜시스 거스리가 1852년에 추측했고, 애플과 하켄이 1976년에 1,936개의 구성을 컴퓨터로 확인하여 증명했다. 이는 컴퓨터 보조 증명으로 완성된 최초의 주요 정리였다. 1997년 로버트슨, 샌더스, 시모어, 토머스는 이를 633개 구성으로 줄여 더 짧은 검증을 제시했다. 이 정리는 토러스 위에서는 성립하지 않으며, 그 경우 일곱 가지 색이 필요할 수 있다.