4색 정리(Four Color Theorem)는 평면상의 어떤 지도라도 인접한 영역을 서로 다른 색으로 칠할 때, 오직 네 가지 색만 있으면 충분하다는 정리다. 1852년 영국의 수학자 프랜시스 구스리(Francis Guthrie)가 지도를 색칠하다가 발견하여 스승인 오거스터스 드 모르간에게 질문하면서 처음 제기되었다. 이 문제는 보기에는 매우 단순해 보이지만, 이를 수학적으로 완벽하게 증명하기까지는 약 120년 이상의 시간이 소요되었다.

이 정리에서 '인접하다'는 것은 두 영역이 점 하나가 아닌, 일정한 길이의 경계선을 공유하는 경우를 의미한다. 만약 점 하나에서만 만나는 경우에는 같은 색을 사용해도 무방하다고 간주한다. 또한 지도의 각 영역은 반드시 하나로 연결되어 있어야 하며, 한 국가가 떨어진 영토를 가지는 예외적인 상황은 고려하지 않는다. 4색 정리는 위상수학적 성질을 가지므로 지도의 구체적인 크기나 모양보다는 영역 간의 연결 상태가 핵심이 된다.

문제 제기 이후 수많은 수학자가 증명에 도전했다. 1879년 앨프리드 켐프(Alfred Kempe)가 증명을 발표하여 한동안 해결된 것으로 여겨졌으나, 1890년 퍼시 히우드(Percy Heawood)가 켐프의 증명에서 결정적인 오류를 발견하며 다시 미해결 상태로 돌아갔다. 히우드는 켐프의 논리를 보완하여 다섯 가지 색이면 충분하다는 '5색 정리'를 증명하는 데는 성공했으나, 네 가지 색에 대한 확답은 얻지 못했다.

결국 4색 정리는 1976년 일리노이 대학교의 케네스 아펠(Kenneth Appel)과 볼프강 하켄(Wolfgang Haken)에 의해 마침내 증명되었다. 이들은 지도의 수많은 형태를 약 1,500여 개의 기본적인 표준형으로 분류한 뒤, 컴퓨터를 사용하여 모든 경우의 수를 일일이 확인하는 방식을 취했다. 이는 수학 역사상 최초로 컴퓨터를 이용해 증명된 주요 정리로 기록되었으며, 당시 수학계에 새로운 패러다임을 제시했다.

컴퓨터를 이용한 증명 방식은 발표 직후 거센 논란을 불러일으키기도 했다. 전통적인 수학적 증명은 사람이 논리적 단계를 직접 검토하고 이해할 수 있어야 한다는 믿음이 지배적이었기 때문이다. 그러나 1997년 닐 로버트슨(Neil Robertson) 등이 더욱 간결한 알고리즘으로 재증명에 성공하고, 이후 컴퓨터 프로그램의 무결성을 검증하는 자동 증명 검사기 등을 통해 타당성이 입증되면서 현재는 보편적인 수학적 사실로 받아들여지고 있다.