4색 정리

4색 정리(Four color theorem, 四色定理)는 어떤 지도든 인접한 지역이 같은 색을 가지지 않도록 하면서 최대 4가지 색만으로 구분할 수 있다는 정리이다.

개요

4색 정리는 평면 또는 구면 위의 임의의 분할된 영역(예: 국가, 주 등)에서 인접한 두 영역이 같은 색을 가지지 않도록 색칠할 때, 단 4가지 색만으로 가능하다는 내용을 담고 있다. "인접"이란 두 지역이 경계를 공유하는 경우를 말하며, 점만 공유하는 경우는 인접으로 보지 않는다. 이 정리는 그래프 이론에서 평면 그래프의 정점 색칠 문제로 등가적으로 변환될 수 있다.

역사

4색 정리는 1852년 프랜시스 거스리(Francis Guthrie)가 제기한 문제에서 출발했다. 이후 수십 년간 수많은 수학자들이 시도했으며, 1976년 케네스 아펠(Kenneth Appel)과 볼프강 하켄(Wolfgang Haken)이 컴퓨터 보조 증명을 통해 정리를 증명하였다. 이는 수학 역사상 최초로 대규모 계산이 증명의 핵심 도구로 사용된 사례로 주목받았다.

수학적 의미

4색 정리는 평면 그래프에 대해 색수(Chromatic number)가 최대 4임을 보장하는 정리로 해석된다. 다시 말해, 어떤 평면 그래프도 인접한 정점이 같은 색을 가지지 않도록 정점을 색칠하는 데에 4가지 색을 넘지 않는다. 이와 달리, 일반적인 그래프 색칠 문제에서는 색수가 훨씬 커질 수 있다.

알고리즘적 접근

4색 정리는 존재 정리이지만, 실제로 색칠하는 알고리즘의 구현에도 영향을 미쳤다. 아펠과 하켄의 증명은 1,936개의 "불가능 구성"을 포함한 경우의 수를 컴퓨터로 전수 조사하는 방식으로 이루어졌으며, 이후 더 간결한 증명과 효율적인 색칠 알고리즘이 개발되었다.

논쟁 및 영향

초기의 컴퓨터 보조 증명은 수학적으로 완전하지 않다는 비판도 받았으며, 사람이 검증할 수 없는 수많은 계산을 포함한다는 점에서 새로운 형식의 수학적 엄밀성에 대한 논의를 불러일으켰다. 이후 증명의 안정성과 재현성 확보를 위한 노력이 계속되었으며, 2005년에는 Gonthier가 Coq 정리 증명기를 이용하여 공식화된 증명을 제공하였다.

같이 보기

• 그래프 색칠 문제
• 평면 그래프
• 컴퓨터 보조 증명
• NP-완전 문제

참고 문헌

• Appel, K., & Haken, W. (1977). Every Planar Map is Four Colorable. *Illinois Journal of Mathematics*, 21(3), 429–567.
• Gonthier, G. (2008). Formal Proof—The Four-Color Theorem. *Notices of the American Mathematical Society*, 55(11), 1382–1393.