지도에서 국경을 맞댄 두 지역을 서로 다른 색으로 표시하려면 몇 가지 색이 필요할까요? 4색 정리(Four Color Theorem)는 평면 위의 어떤 지도라도 네 가지 색이면 충분하다고 말합니다. 단, 두 지역이 선분처럼 길이가 있는 경계를 공유할 때만 이웃으로 셉니다. 꼭짓점 하나에서 만난 지역은 같은 색을 써도 됩니다. 문장은 초등 퍼즐처럼 짧지만, 1852년에 제기된 뒤 1976년에 이르러서야 컴퓨터의 도움을 받은 증명이 완성됐습니다.
지도 색칠을 평면 그래프로 바꾸기
수학에서는 지도의 모양과 넓이를 그대로 다루기보다 이웃 관계만 남깁니다. 지역마다 정점 하나를 놓고, 경계를 공유하는 두 지역의 정점을 간선으로 연결합니다. 그러면 간선이 서로 교차하지 않게 평면에 그릴 수 있는 평면 그래프가 됩니다. 지도 색칠은 이 그래프에서 간선으로 연결된 두 정점에 다른 색을 주는 정점 채색 문제와 같습니다.
4색 정리: 모든 유한한 루프 없는 평면 그래프는 인접한 정점의 색이 다르도록 최대 네 색으로 정점 채색할 수 있습니다.
여기서 ‘최대 네 색’은 모든 지도에 반드시 네 색이 필요하다는 뜻이 아닙니다. 두 색이나 세 색으로 충분한 지도도 많습니다. 정리가 보장하는 것은 아무리 복잡한 평면 지도라도 다섯 번째 색을 요구하지 않는다는 사실입니다. 또 한 지역이 떨어진 여러 조각으로 이루어진 현실의 행정지도는 각 조각을 어떻게 같은 지역으로 취급할지 먼저 정해야 하므로, 정리의 표준 조건과 실제 지도 제작 조건을 구분해야 합니다.
모서리에서 만나는 지역은 왜 이웃이 아닌가
네 지역이 한 점에서만 만나는 지도를 생각해 보겠습니다. 그 점을 지나는 경계선의 길이는 0이므로 서로 국경을 공유한다고 보지 않습니다. 이 규칙을 빼면 정점 하나에 수많은 지역을 모아 놓고 모두 다른 색을 요구할 수 있어 문제 자체가 달라집니다. 그래프 표현에서도 길이 있는 공통 경계를 가진 지역 사이에만 간선을 놓습니다.
프랜시스 거스리의 질문에서 시작된 역사
1852년 영국의 프랜시스 거스리는 잉글랜드의 주 지도를 칠하다가 네 색이면 언제나 충분한지 질문했습니다. 동생 프레더릭을 거쳐 수학자 오거스터스 드모건에게 문제가 전달됐습니다. 1879년 앨프리드 켐프가 증명을 발표했고 한동안 정리된 문제로 여겨졌지만, 1890년 퍼시 히우드가 논리의 빈틈을 찾아냈습니다. 히우드는 켐프의 아이디어를 일부 살려 다섯 색이면 충분하다는 5색 정리를 증명했습니다.
켐프의 실패는 4색 정리가 거짓이라는 뜻이 아니었습니다. 특정 색 두 개로 이어진 경로를 바꾸는 ‘켐프 사슬’ 논증이 모든 경우에 작동하지 않았다는 뜻입니다. 이후 연구자들은 평면 그래프의 국소적인 배열 가운데 어떤 것이 가장 작은 반례에 나타날 수 없는지 조사했습니다. 이 과정에서 환원 가능한 배치와 불가피한 집합이라는 두 개념이 증명의 중심이 됐습니다.
최소 반례를 가정하는 증명 전략
4색으로 칠할 수 없는 평면 그래프가 있다고 가정하면, 그중 정점 수가 가장 적은 최소 반례를 고를 수 있습니다. 이 그래프에서 일부 구조를 더 작은 그래프로 줄인 뒤 그 색칠을 원래 그래프로 되돌릴 수 있다면 모순이 생깁니다. 최소 반례보다 작은 그래프는 정의상 네 색으로 칠할 수 있기 때문입니다. 이렇게 최소 반례에 들어갈 수 없는 국소 구조를 환원 가능한 배치라고 부릅니다.
하지만 환원 가능한 배치를 몇 개 찾는 것만으로는 부족합니다. 가능한 최소 반례가 그 배치들을 모두 피할 수도 있기 때문입니다. 따라서 모든 최소 반례가 반드시 그중 적어도 하나를 포함한다는 ‘불가피성’도 보여야 합니다. 불가피한 집합의 모든 구성원이 동시에 환원 가능하다면 최소 반례는 반드시 포함해야 하는 구조를 포함할 수 없게 되고, 최소 반례가 존재한다는 가정이 무너집니다.
방전법이 불가피한 배치를 찾는 방식
평면 그래프에는 오일러 공식 V−E+F=2에서 비롯되는 평균 차수 제약이 있습니다. 삼각형 면들로 채운 평면 그래프에서는 모든 정점의 차수가 6 이상일 수 없습니다. 방전법(discharge method)은 각 정점이나 면에 차수에 따른 가상의 전하를 배정하고, 정해진 규칙으로 전하를 이웃에게 옮깁니다. 전체 전하 합은 보존되지만 특정 나쁜 배치가 전혀 없다고 가정하면 마지막 전하 상태가 전체 합과 양립하지 않음을 보이는 방식입니다.
방전은 전기를 실제로 계산하는 물리 모형이 아닙니다. 국소적인 차수 정보를 장부처럼 옮겨 적는 조합론적 논증입니다. 이 방법으로 최소 반례라면 피할 수 없는 구성들의 목록을 만들고, 별도의 환원성 검사로 각 구성이 최소 반례에 나타날 수 없음을 확인합니다.
1976년 Appel–Haken 증명에서 컴퓨터가 맡은 일
케네스 아펠과 볼프강 하켄은 1976년 이 전략을 완성했습니다. John Koch도 알고리즘 작업에 기여했습니다. 이들의 증명은 무수한 지도를 하나씩 칠해 본 실험이 아닙니다. 사람이 평면 그래프 이론으로 문제를 유한한 구성 목록으로 줄였고, 컴퓨터가 각 구성의 환원 가능성을 정해진 절차에 따라 검사했습니다. 초기 발표와 후속 정리 과정에서 목록과 프로그램은 수정됐으며, 널리 알려진 완성된 설명에서는 1,936개의 구성이 언급됩니다.
핵심은 ‘많이 확인했으니 아마 참’이라는 통계적 추측과 다르다는 점입니다. 논리적으로 모든 최소 반례가 목록 안의 구성을 포함함을 보이고, 목록의 각 항목이 최소 반례에 들어갈 수 없음을 확인했으므로 반례의 자리가 남지 않습니다. 컴퓨터 계산은 유한하지만 사람이 손으로 전 과정을 따라가기에는 매우 길었던 환원성 검사를 수행했습니다.
컴퓨터 보조 증명이 논쟁을 부른 이유
전통적인 수학 증명은 전문가가 논증의 각 단계를 읽고 확인할 수 있다는 기대를 갖습니다. Appel–Haken 증명은 일부 검사가 프로그램 실행에 의존했고, 사람에게 맡겨진 부분도 길고 복잡했습니다. 그래서 프로그램·하드웨어 오류 가능성과 증명의 이해 가능성을 놓고 논쟁이 생겼습니다. 이는 정리가 경험적으로만 확인됐다는 뜻이 아니라, 계산을 포함한 증거를 어떤 방식으로 독립 검증할 것인가라는 새로운 질문이었습니다.
1996년의 더 단순한 새 증명
Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas는 1996년 미국수학회 학술지에 새로운 증명을 발표했습니다. 이 증명도 컴퓨터를 사용하지만 Appel–Haken 증명보다 불가피한 구성 집합과 환원성 검사를 단순화했습니다. 연구진은 633개의 구성으로 이루어진 집합을 사용했고, 독립적으로 실행하고 점검할 수 있도록 프로그램과 데이터를 제공했습니다. 컴퓨터 의존성을 없애지는 않았지만 검증 부담을 크게 낮췄습니다.
Coq 형식 검증이 더한 확인
Georges Gonthier 연구팀은 2005년 무렵 4색 정리의 형식 증명을 완성했습니다. Coq 증명 보조기 안에서 정의와 보조정리, 계산 절차를 형식 언어로 표현하고 작은 논리 커널이 전체 증명 항목을 검사했습니다. 이는 앞선 실행 결과를 단순히 다시 계산한 것이 아니라, 증명에 필요한 수학과 계산을 기계가 확인할 수 있는 형식으로 연결한 작업입니다.
형식 검증에도 소프트웨어와 하드웨어에 대한 신뢰가 전혀 사라지는 것은 아닙니다. 다만 믿어야 할 코드의 핵심을 작은 커널로 좁히고, 동일한 형식 증명 객체를 다른 사람이 다시 검사할 수 있게 합니다. 이 때문에 4색 정리는 컴퓨터 보조 증명과 형식 증명의 역사에서 모두 중요한 사례로 다뤄집니다.
네 색이 실제로 필요한 지도
세 색으로는 부족한 평면 그래프도 있습니다. 정점 네 개가 서로 모두 연결된 완전그래프 K4는 평면에 간선 교차 없이 그릴 수 있고, 모든 정점 쌍이 인접하므로 네 색이 필요합니다. 지도로 옮기면 서로 두 지역씩 모두 경계를 공유하도록 배치할 수 있습니다. 따라서 ‘네 색이면 충분하다’의 4는 단순한 느슨한 상한이 아니라 어떤 지도에서는 실제로 필요한 최솟값입니다.
평면이 아닌 표면에서는 답이 달라집니다
4색 정리는 평면 또는 구면 위의 지도에 관한 정리입니다. 구면의 한 점을 뚫어 평면으로 펼치는 입체사영을 생각하면 두 경우의 이웃 관계가 같기 때문입니다. 도넛 모양인 토러스처럼 손잡이가 있는 표면에서는 더 많은 색이 필요할 수 있습니다. 또 간선이 교차하는 일반 그래프에는 네 색 상한이 적용되지 않습니다. 예를 들어 K5는 다섯 정점이 서로 모두 인접해 다섯 색이 필요하며 평면 그래프가 아닙니다.
색칠 문제와 실제 알고리즘
정리는 네 색칠의 존재를 보장하지만, 임의의 지도를 사람이 곧바로 예쁘게 칠하는 간단한 규칙 하나를 준다는 뜻은 아닙니다. 평면 그래프를 실제로 네 색칠하는 알고리즘 연구는 증명과 별개로 이어졌습니다. 실무 지도에서는 색각 접근성, 바다와 국경의 표시, 한 지역의 떨어진 영토, 인쇄 대비 같은 제약이 더해지므로 수학적 최소 색 수와 디자인에 쓰는 색 수가 다를 수 있습니다.
자주 생기는 오해
- 꼭짓점 하나에서만 만난 지역은 표준 4색 문제에서 이웃이 아닙니다.
- 모든 지도에 네 색이 꼭 필요한 것은 아니며, 네 색은 어떤 지도에도 충분한 최댓값입니다.
- 1976년 증명은 가능한 모든 지도를 무작정 컴퓨터로 생성한 실험이 아닙니다.
- 4색 정리는 평면 그래프에 적용되며 모든 그래프의 채색수를 네 이하로 제한하지 않습니다.
- 컴퓨터가 사용됐다는 사실은 확률적 근사라는 뜻이 아닙니다. 증명은 유한한 경우의 완전한 논리적 검사를 포함합니다.
4색 정리 핵심 정리
지역을 정점으로, 공통 경계를 간선으로 바꾸면 지도 색칠은 평면 그래프의 정점 채색이 됩니다. 4색 정리는 이 그래프를 언제나 네 색 이하로 칠할 수 있다고 말합니다. 증명은 최소 반례를 가정한 뒤, 그 반례에 반드시 나타나는 불가피한 구성과 나타날 수 없는 환원 가능한 구성이 같은 목록임을 보여 모순을 얻습니다.
Appel과 Haken은 1976년 컴퓨터 검사를 이용해 첫 증명을 완성했습니다. 1996년 Robertson·Sanders·Seymour·Thomas가 더 단순한 컴퓨터 보조 증명을 제시했고, 이후 Coq를 이용한 형식 검증도 이루어졌습니다. 따라서 오늘날 4색 정리는 증명된 정리이며, 동시에 컴퓨터가 수학적 증거를 어떻게 확인할 수 있는지 보여 주는 대표 사례입니다.