수학의 역사에서 가장 유명하면서도 동시에 가장 큰 논란을 불러일으킨 정리 중 하나가 바로 ‘4색 정리(Four Color Theorem)‘입니다. “어떠한 평면 지도라도 인접한 영역이 서로 다른 색이 되도록 칠하는 데에는 4색이면 충분하다"는, 초등학생도 이해할 수 있을 만큼 단순한 주장이지만, 그 증명에는 1세기 이상의 세월과 수학이라는 학문의 근간을 뒤흔든 ‘컴퓨터에 의한 증명’이라는 패러다임 전환이 필요했습니다.

본고에서는 1852년의 소박한 의문에서 시작하여 천재들의 도전과 좌절, 그리고 컴퓨터라는 새로운 지성을 아군으로 삼은 현대 수학의 도달점에 이르기까지 4색 정리의 전모를 수학적, 역사적, 철학적 관점에서 철저하게 해설합니다. 특히 켐프의 거짓 증명과 히우드의 반례가 가지는 기하학적 구조, 5색 정리의 완전한 증명, 방전법의 수리, 아펠과 하켄의 알고리즘, Coq를 이용한 형식 증명의 세부 내용, 그리고 NP-완전성과의 관련성이라는 심오한 수학적 주제에 깊이 들어가 설명합니다.

제1장: 1852년, 프랜시스 구스리의 소박한 의문과 그래프 이론으로의 승화

지도 색칠 문제의 제기

이야기의 시작은 1852년, 영국의 유니버시티 칼리지 런던을 막 졸업한 청년 프랜시스 구스리(Francis Guthrie)로 거슬러 올라갑니다. 그는 영국의 주 지도를 색칠하던 중 어떤 기묘한 사실을 깨달았습니다. “아무리 복잡한 지도라도 인접한 주가 서로 다른 색이 되도록 칠하는 데에는 4색이면 충분하지 않을까?”

프랜시스는 이 의문을 당시 유니버시티 칼리지에서 수학을 배우고 있던 동생 프레더릭 구스리(Frederick Guthrie)에게 털어놓았습니다. 프레더릭은 자신의 지도교수이자 당시를 대표하는 수학자 중 한 명이었던 오거스터스 드 모르간(Augustus De Morgan)에게 이 문제를 제시합니다. 드 모르간은 즉시 이 문제의 재미에 이끌려 친구인 윌리엄 로언 해밀턴(William Rowan Hamilton) 등에게 편지로 이 문제를 공유했습니다. 이것이 수학사에 찬란히 빛나는 ‘4색 문제’가 탄생한 순간입니다.

오일러의 다면체 정리와 평면 그래프의 쌍대성

지도 색칠 문제를 수학적으로 엄밀하게 다루기 위해서는 그래프 이론으로의 공식화가 필수적입니다. 지도 상의 각 영역(국가나 주)을 ‘정점(Vertex)‘으로 하고, 인접한 영역끼리 ‘간선(Edge)‘으로 연결하면 평면상에서 간선이 교차하지 않는 ‘평면 그래프(Planar Graph)‘를 얻을 수 있습니다. 이 변환은 ‘쌍대 그래프(Dual Graph)‘를 취하는 조작으로 알려져 있습니다. 원래 지도의 경계선이 그래프의 간선에, 면이 정점에 대응합니다.

4색 문제는 “임의의 평면 그래프의 정점을, 인접한 정점이 서로 다른 색이 되도록 4색으로 칠할 수 있는가"라는 그래프의 정점 색칠 문제(Vertex Coloring Problem)로 귀결됩니다.

여기서 매우 중요한 역할을 하는 것이 레온하르트 오일러가 발견한 다면체 정리입니다. 연결된 평면 그래프에서 정점의 수를 $V$, 간선의 수를 $E$, 면의 수를 $F$라고 하면, 다음과 같은 불변의 관계가 성립합니다.

이 정리와 평면 그래프의 기본적인 성질을 결합하면 평면 그래프의 구조에 관한 강력한 제약을 이끌어낼 수 있습니다. 그래프에 다중 간선이나 루프가 없는 단순 그래프라고 가정하고, 나아가 모든 면이 삼각형인 ‘극대 평면 그래프(Maximal Planar Graph)‘를 생각합니다. 임의의 평면 그래프는 간선을 추가하여 극대 평면 그래프로 만들어도 색칠에 필요한 색의 수는 늘어나지 않으므로, 극대 평면 그래프에 대해서만 4색 정리를 증명하면 충분합니다.

극대 평면 그래프에서 각 면은 정확히 3개의 간선으로 둘러싸여 있습니다. 1개의 간선은 정확히 2개의 면의 경계가 되므로, 면의 수와 간선의 수 사이에는 다음의 관계가 엄밀하게 성립합니다.

이것을 오일러의 공식에 대입하여 $F$를 소거합니다. $F = \frac{2}{3}E$를 $V - E + F = 2$에 대입하면,

일반적인 단순 평면 그래프에서는 면이 3개 이상의 간선으로 둘러싸이므로 $3F \leq 2E$가 되어 다음 부등식이 도출됩니다.

이 부등식은 평면 그래프의 간선 밀도에 엄밀한 상한이 있음을 보여줍니다. 여기서 각 정점의 차수(Degree, $\deg(v)$)에 대해 생각해 봅시다. 그래프의 모든 정점의 차수의 합은 간선의 수의 정확히 2배가 됩니다(악수 보조정리).

앞서 도출한 부등식 $2E \leq 6V - 12$를 이용하면,

양변을 정점 수 $V$로 나누면 정점의 평균 차수를 얻을 수 있습니다.

평균 차수가 엄밀히 6 미만이라는 것은 “적어도 1개의 정점은 차수가 5 이하여야 한다"는 것을 수학적으로 완전히 증명합니다. 즉, 임의의 단순 평면 그래프에는 차수가 1, 2, 3, 4, 5 중 하나인 정점이 적어도 하나 존재합니다. 이 사실은 후술할 ‘불가피한 배열’ 개념의 가장 기초적인 출발점이며, 4색 정리 증명의 절대적인 핵심이 됩니다.

제2장: 알프레드 켐프의 ‘증명’과 11년 후의 붕괴

켐프 사슬의 개념과 화려한 ‘증명’

1879년, 영국의 변호사이자 수학자이기도 했던 알프레드 브레이 켐프(Alfred Kempe)가 마침내 4색 문제의 ‘증명’을 《Nature》지와 《American Journal of Mathematics》지에 발표했습니다. 그의 증명은 매우 독창적이었으며, 이후 11년 동안 전 세계 수학계에 올바른 것으로 받아들여졌습니다.

켐프 증명의 핵심은 현재 ‘켐프 사슬(Kempe Chain)‘이라고 불리는 획기적인 아이디어였습니다. 그는 수학적 귀납법을 사용했습니다. 정점 수가 $k$인 모든 평면 그래프에서 4색 정리가 성립한다고 가정하고, 정점 수가 $k+1$인 그래프에서도 성립함을 보이려고 했습니다.

앞서 언급한 오일러의 정리에 의해, 정점 수 $k+1$인 평면 그래프 $G$에는 반드시 차수가 5 이하인 정점 $v$가 존재합니다. 그래프 $G$에서 정점 $v$와 그것에 연결된 간선을 제거한 그래프 $G'$를 생각합니다. $G'$는 정점 수가 $k$이므로 귀납법의 가정에 의해 4색(여기서는 빨강, 파랑, 초록, 노랑이라고 하겠습니다)으로 색칠할 수 있습니다. 그 후 $v$를 되돌려 색칠을 시도합니다.

1. $v$의 차수가 3 이하인 경우: $v$에 인접한 정점은 최대 3개입니다. 따라서 4색 중 적어도 1색은 인접한 정점에 사용되지 않았습니다. 그 사용되지 않은 색을 $v$에 칠하면 증명 완료입니다.
2. $v$의 차수가 4인 경우: $v$에 인접한 4개의 정점(시계방향으로 $v_1, v_2, v_3, v_4$라고 합시다)이 모두 다른 색(빨강, 파랑, 초록, 노랑)으로 칠해져 있다고 가정합니다. 여기서 그래프 전체에서 ‘빨강’과 ‘초록’으로 칠해진 정점들과 그들을 연결하는 간선만을 추출한 부분 그래프를 생각합니다. 만약 $v_1$(빨강)과 $v_3$(초록)이 이 빨강-초록 부분 그래프 안에서 연결되어 있지 않다면(즉, 빨강과 초록 정점을 따라 $v_1$에서 $v_3$으로 가는 경로가 존재하지 않는다면), $v_1$을 포함하는 연결 성분의 색을 반전(빨강을 초록으로, 초록을 빨강으로)시킬 수 있습니다. 이를 ‘켐프 사슬의 반전’이라고 부릅니다. 반전 후 $v_1$은 초록이 되고, 주변의 색은 파랑, 초록, 초록, 노랑의 3색으로 줄어듭니다. 이로써 $v$에 빨강을 칠할 수 있게 됩니다. 만약 $v_1$과 $v_3$이 연결되어 있다면 평면 그래프의 위상적 성질(조르당 폐곡선 정리)에 의해 $v_1$과 $v_3$을 잇는 빨강-초록 경로가 $v_2$(파랑)와 $v_4$(노랑)를 분단합니다. 따라서 $v_2$와 $v_4$는 파랑-노랑 켐프 사슬로 절대 연결될 수 없으며, $v_2$를 포함하는 파랑-노랑 성분을 반전시킬 수 있습니다. 어느 쪽이든 $v$ 주변의 색을 3색으로 줄일 수 있어 $v$를 색칠할 수 있습니다.
3. $v$의 차수가 5인 경우: $v$ 주변의 5개 정점 $v_1, v_2, v_3, v_4, v_5$가 각각 빨강, 파랑, 초록, 노랑, 빨강(5개이므로 1색은 중복됨)으로 칠해져 있는 경우 등을 생각합니다. 켐프는 차수가 4인 경우의 논법을 확장하여, 2개의 다른 켐프 사슬(예를 들어 빨강-초록 사슬과 빨강-노랑 사슬)의 반전을 교묘하게 조합하면 반드시 $v$ 주변의 색을 3색 이하로 줄일 수 있다고 주장했습니다. 그의 방법은 한쪽이 연결되어 있다면 다른 쪽은 분단된다는 논리를 이중으로 적용하는 것이었습니다.

이 증명은 직관적이고 아름다웠으며 논리의 빈틈이 없어 보였습니다. 당시 수학자들은 이것으로 4색 문제가 완전히 해결되었다고 믿어 의심치 않았습니다.

히우드의 반례 그래프: ‘이중 켐프 사슬의 교차’라는 치명적 결함

그러나 1890년, 당시 29세였던 퍼시 존 히우드(Percy John Heawood)라는 수학자가 켐프의 논문을 정독하고 차수가 5인 정점에 관한 논증에서 치명적인 논리의 비약을 발견했습니다.

켐프는 2개의 켐프 사슬(예를 들어 파랑-초록 사슬과 파랑-노랑 사슬)의 반전을 각각 수행할 때, 그것들이 서로 독립적으로 반전 가능하다고 암묵적으로 가정하고 있었습니다. 하지만 히우드는 이 두 사슬이 일부 정점을 공유하고 있을 경우, 첫 번째 사슬을 반전시킴으로써 그래프의 색칠 상태가 변화하고 두 번째 사슬의 연결성이 바뀌어 버린다는 것을 기하학적이고 엄밀하게 증명했습니다.

히우드는 구체적인 반례 그래프(현재 ‘히우드의 반례(Heawood graph)‘나 그 파생으로 알려진, 25개 정점으로 이루어진 극대 평면 그래프)를 구축했습니다. 이 그래프에서 차수 5인 정점 $v$ 주변의 색을 줄이기 위해 켐프의 알고리즘을 적용하면, 파랑-초록 사슬을 반전시킨 순간에 원래는 연결되어 있지 않던 파랑-노랑 사슬이 연결되어 버리고, 이어서 파랑-노랑 사슬을 반전시키면 앞서 반전시켰던 초록 정점이 다시 원래 색으로 돌아가 버려 결과적으로 색의 수가 줄어들지 않는 루프에 빠진다는 것을 보여주었습니다.

켐프의 ‘이중 켐프 사슬의 동시 교체’는 국소적인 위상의 분단 관계를 대국적으로 유지할 수 없다는, 평면 그래프의 복잡한 얽힘을 과소평가한 결과인 오류였습니다. 이 발견으로 인해 켐프의 4색 정리 증명은 완전히 무너졌습니다.

5색 정리의 수학적 완전 증명

켐프의 증명은 붕괴했지만 히우드는 단지 파괴하기만 한 것이 아닙니다. 그는 켐프의 아이디어(켐프 사슬) 자체는 매우 유용하다는 것을 인식하고, 그것을 사용하여 “모든 평면 그래프는 5색이 있으면 반드시 칠할 수 있다"는 ‘5색 정리(Five Color Theorem)‘를 엄밀하게 증명했습니다. 5색 정리의 완전한 증명 과정은 다음과 같습니다.

정리: 임의의 평면 그래프 $G$는 5색으로 정점 색칠이 가능하다. 증명: 정점 수 $n$에 대한 수학적 귀납법을 사용한다. $n \leq 5$인 경우는 자명하다. $n=k$인 모든 평면 그래프가 5색으로 색칠 가능하다고 가정하고, $n=k+1$인 평면 그래프 $G$를 생각한다. 오일러의 공식에서 도출되는 사실에 의해, $G$에는 반드시 차수가 5 이하인 정점 $v$가 존재한다. $G$에서 $v$를 제외한 그래프 $G' = G - \{v\}$는 정점 수가 $k$이므로 귀납법의 가정에 의해 5색(색1, 색2, 색3, 색4, 색5)으로 색칠 가능하다. $G'$의 색칠 상태를 유지한 채 $v$를 되돌리는 것을 생각한다.

• 케이스 1: $\deg(v) < 5$인 경우. $v$에 인접한 정점은 기껏해야 4개이므로, 5색 중 적어도 1색은 인접 정점에 사용되지 않았다. 그 색을 $v$에 칠하면 된다.
• 케이스 2: $\deg(v) = 5$인 경우. $v$에 인접한 5개의 정점 $v_1, v_2, v_3, v_4, v_5$(시계방향으로 배치)가 모두 다른 색(순서대로 색1, 색2, 색3, 색4, 색5)으로 칠해져 있다고 가정한다. (만약 같은 색이 2번 이상 사용되었다면 사용되지 않은 색이 1색 이상 남으므로 그것을 $v$에 칠할 수 있다). 여기서 그래프 $G'$에 대해, 색1과 색3으로 칠해진 정점으로만 이루어진 유도 부분 그래프를 생각하고, 그중 $v_1$을 포함하는 연결 성분을 $C_{13}$이라고 하자(이것이 켐프 사슬이다).
  • 서브케이스 2a: $v_3 \notin C_{13}$인 경우. 즉, $v_1$에서 $v_3$으로 색1과 색3의 정점만 통과하는 경로가 존재하지 않는 경우. 이때 $C_{13}$ 안의 모든 정점의 색을 반전(색1 $\leftrightarrow$ 색3)시켜도 색칠의 정당성은 유지된다. 반전 후 $v_1$은 색3이 되고, $v_3$도 색3이므로 $v$ 주변에는 색1이 존재하지 않게 된다. 따라서 $v$에 색1을 칠할 수 있다.
  • 서브케이스 2b: $v_3 \in C_{13}$인 경우. 즉, $v_1$과 $v_3$을 잇는 색1과 색3의 정점으로 이루어진 경로 $P_{13}$이 존재하는 경우. 이 경로 $P_{13}$과 정점 $v$, 그리고 간선 $(v, v_1), (v, v_3)$을 합치면 평면상에 폐곡선(사이클)이 형성된다. 평면 그래프의 성질(조르당 폐곡선 정리)에 의해 이 사이클은 평면을 안쪽과 바깥쪽으로 분단한다. 정점 $v_2$와 $v_4$는 이 사이클의 다른 쪽(하나는 안쪽, 다른 하나는 바깥쪽)에 위치한다. 여기서 색2와 색4로 칠해진 정점들로 이루어진 켐프 사슬 $C_{24}$를 생각한다. $v_2$와 $v_4$가 이 사슬로 연결되어 있다고 가정하면 $v_2$와 $v_4$를 잇는 경로 $P_{24}$가 존재해야 한다. 그러나 $P_{24}$는 평면 그래프 위를 교차하지 않고 지나가야 하는데, $P_{13}$에 의해 형성된 사이클을 가로지를 수 없다(평면 그래프의 정의에 위배됨). 따라서 $v_2$와 $v_4$를 잇는 색2와 색4의 경로는 절대 존재하지 않는다. 즉, $v_2$를 포함하는 색2-색4 켐프 사슬 $C_{24}$에는 $v_4$가 포함되지 않는다. 그러므로 $C_{24}$ 내의 색을 반전(색2 $\leftrightarrow$ 색4)시키면 $v_2$는 색4가 되고, $v$ 주변에서 색2가 소멸한다. 최종적으로 $v$에 색2를 칠할 수 있다.

이상으로 어떠한 경우에도 $v$를 색칠할 수 있으며, 수학적 귀납법에 의해 5색 정리가 완전히 증명되었다. $\blacksquare$

이 증명은 평면 그래프의 위상(조르당 폐곡선 정리)을 매우 아름답게 이용한 것으로, 켐프의 ‘켐프 사슬’이라는 개념이 단일한 교차하지 않는 사슬의 적용에 있어서는 얼마나 강력한지를 보여줍니다. 그러나 ‘4색’으로 가는 길은 여기서부터 ‘가약성(Reducibility)‘과 ‘불가피 집합(Unavoidable Set)‘이라는 새로운 패러다임을 거쳐 엄청난 계산의 바다로 뛰어들게 됩니다.

제3장: 방전법(Discharging Method)의 수리와 불가피 배열의 도출

히우드 이후 수학자들은 ‘4색으로 칠할 수 없는 최소의 반례(Minimum Counterexample)‘가 존재한다고 가정하고, 그것이 어떤 구조를 가져야 하는지(또는 가지지 않아야 하는지)를 귀류법으로 탐구하기 시작했습니다. 여기서 중요해지는 것이 ‘가약 배열(Reducible Configuration)‘과 ‘불가피 집합(Unavoidable Set)‘이라는 두 가지 강력한 개념입니다.

가약성(Reducibility)

가약 배열이란 “만약 그래프 전체가 4색으로 칠해지지 않는다면(최소의 반례라면), 그 그래프 안에는 절대 존재할 수 없는” 정점의 국소적인 부분 배열(패턴)을 말합니다. 예를 들어 ‘차수가 3 이하인 정점’이나 ‘차수가 4인 정점’은 가약 배열입니다. 왜냐하면 앞서 말한 것처럼 켐프 사슬에 의한 환원을 사용하면 만약 그것들이 존재했을 때 더 작은 그래프 문제로 귀착(환원)시킬 수 있어, ‘최소의 반례’라는 가정과 모순되기 때문입니다. 1913년 조지 데이비드 버코프(George David Birkhoff)는 ‘버코프의 다이아몬드’라고 불리는 특정한 6개의 정점으로 이루어진 배열도 가약임을 증명했습니다. 가약 배열의 발견은 계속되었지만, 그것들이 그래프 안에 ‘반드시 존재한다’는 것을 보장하지 못하면 증명에는 이르지 못합니다.

방전법(Discharging Method)의 수리 구조

4색 정리를 증명하기 위한 최종 전략은 **“그 전부가 가약 배열로 구성된, 불가피 집합을 찾는 것”**으로 집약됩니다. 불가피 집합이란 “어떤 평면 그래프(더 정확하게는 극대 평면 그래프)에도 그 집합 안의 적어도 하나의 배열이 반드시 포함되는” 배열의 리스트입니다.

이 불가피 집합을 구축하고 증명하기 위한 극히 강력한 무기가 바로 하인리히 헤쉬(Heinrich Heesch)에 의해 세련된 ‘방전법(Discharging Method)‘입니다. 방전법은 그래프 이론에서 구조 정리를 증명하기 위한 마법과도 같은 기법으로, 전자기학의 전하 개념을 유추하여 사용합니다.

방전법의 수리적 과정은 다음과 같습니다.

1. $$ch(v) = 6 - \deg(v)$$

   오일러의 공식에서 도출된 등식 $\sum_{v} (6 - \deg(v)) = 12$에 의해 그래프 전체의 초기 전하의 총합은 엄밀하게 12(양수 값)가 됩니다. 이때 차수 5인 정점은 $+1$, 차수 6인 정점은 $0$, 차수 7 이상인 정점은 음의 전하를 가집니다. (최소의 반례에는 차수 4 이하인 정점은 존재하지 않는다고 가정할 수 있으므로 최소 차수는 5로 생각합니다).

2. 전하 이동 규칙(Discharging Rules)의 정의: 다음으로, 전하를 인접한 정점 간에 이동시키는 규칙을 정의합니다. 기본적인 사고방식은 “양의 전하를 가진 정점(즉 차수 5의 정점)에서 음의 전하를 가진 정점(차수 7 이상의 고차수 정점)으로 전하를 흘려보낸다(방전한다)“는 것입니다. 예를 들어 “차수 5인 정점 $v$가 차수 7인 정점 $u$와 인접해 있는 경우, $v$에서 $u$로 $\frac{1}{5}$의 전하를 이동시킨다"와 같은 규칙을 수십, 수백 가지로 세밀하게 설정합니다.

3. $$ \sum_{v \in V} ch'(v) = 12 > 0 $$

   ($ch'(v)$는 이동 후의 정점 $v$의 전하) 전체 합이 양수라는 것은 **“전하 이동 후에도 양의 전하를 가진 정점이 적어도 하나는 존재해야 한다”**는 것을 의미합니다.

   여기서 각 정점의 최종 전하 $ch'(v)$를 국소적인 구조(그 정점과 인접한 정점 차수의 패턴)에 기반하여 분석합니다. 만약 “어떤 특정 배열을 가지지 않는 정점은 설정한 방전 규칙 아래에서 반드시 최종 전하가 0 이하가 된다"는 것을 증명할 수 있다면, 최종 전하가 양수가 되기 위해서는 그 ‘특정 배열’이 그래프 내 어딘가에 반드시 존재해야만 하게 됩니다. 이렇게 해서 최종 전하가 양수가 되는 국소적 배열 패턴을 모두 망라하여 리스트업한 것이 ‘불가피 집합’이 되는 것입니다.

헤쉬는 이 방전법을 사용하면 유한 개(아마도 수천 개)의 가약 배열로 이루어진 불가피 집합을 구축할 수 있을 것이라 확신했습니다. 하지만 어떤 배열이 ‘가약’인지를 판정하기 위한 계산량은 경계의 길이에 대해 지수함수적으로 폭발합니다. 인간의 손 계산으로는 수천 개 배열의 가약성을 체크하는 것은 수명이 다해도 불가능했습니다.

제4장: 1976년, 아펠과 하켄의 컴퓨터 검증 알고리즘

D-환원과 C-환원의 정의

1970년대, 일리노이 대학교의 케네스 아펠(Kenneth Appel)과 볼프강 하켄(Wolfgang Haken)은 헤쉬의 방전법과 컴퓨터의 계산 능력을 융합시키는 역사적인 프로젝트에 착수했습니다.

그들이 다룬 가장 계산량이 무거운 작업은 배열의 ‘가약성 판정’입니다. 가약성에는 주로 두 가지 유형이 있습니다.

• D가약성(D-reducibility / Direct reducibility): 배열을 둘러싼 환형의 경계(Ring)의 모든 가능한 4색 칠하기 패턴에 대해, 그것이 배열 내부로도 확장되어 칠해질 수 있거나 경계 색의 켐프 사슬을 반전시킴으로써 내부로 확장 가능한 패턴으로 변환할 수 있는 경우. 이것이 확인되면 그 배열은 최소의 반례에 포함되지 않는다는 것을 즉각적으로 말할 수 있습니다.
• C가약성(C-reducibility / Contracting reducibility): D가약 판정에서 실패하는 패턴이 존재하는 경우, 그 배열의 일부를 ‘축약(여러 정점을 하나로 찌그러뜨림)‘한 더 작은 그래프를 생각하고, 그 축약 그래프가 4색 가능하면 원래 그래프도 4색 가능함을 보여주는 수법.

환형 경계의 색칠 가능성 판정 알고리즘

컴퓨터(IBM 360)에 맡겨진 것은 방대한 수의 배열 후보에 대한 D가약성 및 C가약성 판정 알고리즘의 실행이었습니다.

어떤 배열 $C$가 경계 링 $R$(길이 $k$)를 가지고 있다고 합시다. 링 위의 정점을 4색으로 칠하는 조합은 최대 $4^k$가지가 있지만 대칭성을 고려해도 엄청난 수가 됩니다. 예를 들어 링의 길이가 $k=14$인 경우 약 20만 가지나 되는 경계 색칠의 유효성을 확인해야 합니다. 알고리즘은 다음 절차로 진행됩니다.

1. 경계 링 $R$의 모든 유효한 4색 패턴 집합을 생성한다.
2. 배열 $C$의 내부를 실제로 4색으로 칠하는 방법을 모두 시도하여 어떤 경계 패턴과 정합하는지(내부 확장 가능한지)를 기록한다.
3. 내부 확장 불가능한 경계 패턴에 대해 켐프 사슬의 반전을 시뮬레이션한다. 반전에 의해 이미 ‘내부 확장 가능’으로 판명된 패턴으로 전이할 수 있으면, 그 초기 패턴도 ‘해결됨’으로 간주한다.
4. 이 반전 전이 탐색을 반복하여 모든 경계 패턴이 해결 가능하면 그 배열 $C$는 ‘D가약’이라고 판정한다.

경계 길이가 길어지면 계산 시간이 폭발하므로, 아펠과 하켄은 링 길이를 최대 14까지인 배열로 제한하고 그 안에서 불가피 집합을 구축하기 위한 방전 규칙을 철저하게 튜닝했습니다. 이 튜닝 과정 자체가 인간과 컴퓨터에 의한 거대한 시행착오의 연속이었습니다. “인간이 방전 규칙을 수정하고 컴퓨터가 불가피 집합 후보를 내며 가약성을 테스트하고, 실패한 배열을 보고 인간이 다시 규칙을 수정한다"는 대화식 과정이 수년에 걸쳐 계속되었습니다.

1200시간의 계산과 ‘Q.E.D.’

1976년, 그들은 마침내 정교하게 구축된 방전 규칙에 의해 도출된 1,936개의 배열로 이루어진 불가피 집합을 발견했습니다. 그리고 일리노이 대학교의 메인프레임을 1200시간 이상 가동시킨 끝에 그 1,936개의 배열 모두가 D가약 또는 C가약임을 컴퓨터가 확인했습니다.

그들은 논문 요약에 짧게 이렇게 적었습니다. “Every planar map is four colorable.”

일리노이 대학교 수학과 우편 스탬프에는 “FOUR COLORS SUFFICE(4색이면 충분하다)“라는 자랑스러운 각인이 새겨졌습니다. 이는 수학 역사상 컴퓨터가 정리 증명에서 핵심적인 연역 단계를 담당한 최초의 기념비적 사건이었습니다.

제5장: 수학계의 격진과 ‘증명’의 철학

아펠과 하켄의 발표는 수학계에 환희보다는 오히려 깊은 당혹감과 격렬한 논쟁을 불러일으켰습니다.

인간이 읽을 수 없는 증명은 수학인가?

고대 그리스부터 이어진 수학의 전통에서 ‘증명’이란 인간 수학자가 논리의 단계를 하나하나 따라가며 그 올바름을 진심으로 이해하고 납득할 수 있는 것이었습니다. 증명 과정에는 “왜 그 정리가 성립하는가"라는 깊은 통찰이나 구조의 아름다움이 깃들어 있다고 믿어왔습니다.

그러나 4색 정리의 증명은 이질적이었습니다. 논문에는 1,936개나 되는 배열 리스트와 컴퓨터 알고리즘에 대한 설명만 있을 뿐입니다. 실제 가약성 판정 추적(실행 기록)은 너무 방대해서 종이에 인쇄하는 것조차 곤란했습니다. 아무리 천재 수학자라도 평생을 바쳐도 그 계산을 손으로 추적하여 논리적 결함이 없음을 확인하는 것은 불가능합니다.

“증명이 올바른지 믿기 위해서는 컴퓨터 하드웨어가 고장 나지 않았다는 것과 아펠과 하켄이 작성한 어셈블리 언어 프로그램에 버그가 없다는 것을 믿어야 한다"는 전대미문의 상황이 벌어졌습니다.

과학철학자 토머스 티모츠코(Thomas Tymoczko)는 이 증명이 순수수학의 선험적(a priori) 진리 탐구에서 물리학과 같은 경험과학적이고 실험적인 것으로 타락한 것은 아닌지 비판했습니다. ‘증명’이라는 행위의 정의 자체가 인식론적인 위기에 처한 것입니다.

반론과 RSST에 의한 간략화

아펠과 하켄은 비판에 대해 “아름다운 증명만이 수학은 아니다. 거대한 경우 나누기가 필요한 본질적으로 복잡한 문제가 존재하며 인간 두뇌의 한계를 넘는다면 기계의 힘을 빌리는 것은 필연적인 진화다"라고 반론했습니다.

이 찜찜함을 해소하기 위해 많은 수학자가 증명의 간략화와 재검증에 도전했습니다. 1997년 닐 로버트슨(Neil Robertson), 대니얼 샌더스(Daniel P. Sanders), 폴 시모어(Paul Seymour), 로빈 토머스(Robin Thomas) 4명(통칭 RSST)은 방전법을 더 체계적이고 인간이 검증하기 쉽게 개량하여 불가피 집합의 크기를 1,936개에서 633개까지 줄인 새로운 증명을 발표했습니다. 계산 시간도 몇 시간 만에 끝나는 세련된 알고리즘이었습니다.

그러나 이것도 여전히 ‘컴퓨터에 의한 가약성 계산’에 의존하고 있다는 점은 변함이 없습니다. 인간의 직관으로 완전히 이해할 수 있는 ‘아름다운 종이와 펜의 증명’은 아직 발견되지 않았습니다. (그리고 그러한 증명은 원리적으로 존재하지 않을 것이라고 많은 그래프 이론 학자들은 생각하고 있습니다).

제6장: Coq에 의한 조르주 공티에의 완전 형식 증명

“프로그램에 버그가 있을지도 모른다"는 불안을 수학적으로 완전히 불식시키기 위해서는 어떻게 해야 할까요? 그 궁극적인 해답이 ‘정리 증명 지원계(Proof Assistant)‘를 이용한 완전한 형식화(Formalization)입니다.

2005년 프랑스 국립 정보학 자동 제어 연구소(INRIA)와 마이크로소프트 리서치의 조르주 공티에(Georges Gonthier)는 뱅자맹 베르네르(Benjamin Werner)와 함께 정리 증명 지원계 ‘Coq’를 사용하여 4색 정리의 증명을 근본부터 완전히 형식화하는 데 성공했습니다.

초준유한사상(Hypermap)과 조합 위상수학의 형식화

Coq는 수학 공리에서 출발하여 매우 엄밀한 논리 규칙 체계(Calculus of Inductive Constructions: 귀납적 구성 계산)에 따라 증명을 기술하고 기계 검증하는 시스템입니다.

공티에의 가장 큰 공적은 평면 그래프라는 직관적이고 기하학적인 대상을 컴퓨터가 다룰 수 있는 완전한 대수적·조합론적 구조로 번역했다는 것입니다. 그는 그래프의 정점, 간선, 면의 관계를 표현하기 위해 ‘초준유한사상(Hypermap)‘이라는 데이터 구조를 정의했습니다. 이것은 그래프를 ‘다트(반쪽 간선)‘의 집합과 그 위의 치환(순열)군으로 표현하는 방법입니다. 이에 의해 오일러의 공식이나 조르당 폐곡선 정리 같은 위상수학의 정리가 군론과 유한집합의 조합 논리로 완전히 형식화되었습니다.

증명 프로그램 자체의 정당성 증명

게다가 공티에는 아펠-하켄이나 RSST가 수행했던 ‘C 언어로 작성된 검증 프로그램’을 버리고 Coq의 내부 언어(Gallina)를 사용하여 가약성을 판정하는 알고리즘 자체를 구현했습니다. 그리고 “이 판정 알고리즘이 ‘True’를 출력한다면 그 배열은 진정으로 가약이다"라는 알고리즘의 정당성 자체를 Coq 상에서 수학적으로 증명한 것입니다.

이로 인해 증명의 신뢰성은 결정적으로 변했습니다. ‘알고리즘의 버그’를 걱정할 필요는 없어졌습니다. 왜냐하면 Coq의 핵심이 되는 논리 검증 커널(수백 줄의 매우 단순하고 검증된 코드, 드 브루인 인덱스 등을 사용하여 구현됨)이 논리적 추론 규칙을 올바르게 처리하고 있는 한, 공티에가 구축한 거대한 증명 트리는 절대적으로 올바르다는 것이 수학적으로 보장되기 때문입니다.

이것은 수학에서 ‘증명’의 새로운 도달점입니다. “인간이 읽고 이해하는 증명(Informal Proof)“에서 “기계가 논리적 완전성을 보장하는 형식 증명(Formal Proof)“으로의 진화입니다. 4색 정리는 역사상 최초로 이 극한의 엄밀성에 도달한 비자명한 대정리가 되었습니다.

제7장: 평면 그래프의 4색칠 문제와 NP-완전성의 역설

마지막으로 4색 정리를 계산 복잡도 이론(Computational Complexity Theory)의 관점에서 살펴봅시다. 여기에는 매우 흥미로운 역설과도 같은 현상이 존재합니다.

일반 그래프에서의 색칠 문제(주어진 그래프를 $k$가지 색으로 칠할 수 있는지 판정하는 문제)는 컴퓨터 과학에서 가장 유명한 ‘NP-완전(NP-complete)’ 문제 중 하나입니다. 특히 ‘평면 그래프의 3색칠 문제(Planar 3-Colorability)‘는 NP-완전임이 증명되어 있습니다. 즉 어떤 평면 그래프를 3색으로 칠할 수 있는지를 다항 시간에 판정하는 알고리즘은 $\text{P} = \text{NP}$가 아닌 한 존재하지 않는다고 여겨지고 있습니다.

그럼 ‘평면 그래프의 4색칠 문제(Planar 4-Colorability)‘는 어떨까요? 3색이 NP-완전이라면 4색도 마찬가지로 어려울 것(NP-완전)이라고 직관적으로는 생각될 수 있습니다.

그러나 놀랍게도 평면 그래프의 4색칠 문제(판정 문제)의 계산 복잡도는 $O(1)$, 즉 ‘상수 시간(자명함)‘입니다. 왜냐하면 4색 정리가 “모든 평면 그래프는 4색으로 칠할 수 있다"고 보장하고 있기 때문에, 알고리즘은 입력된 그래프를 보지도 않고 그저 “Yes"라고 출력하기만 해도 항상 100% 정답이 되기 때문입니다. 이것은 정리의 강력한 존재 보장이 판정 문제의 복잡성을 극한까지 낮춰버린 아름다운 예입니다.

다만 이것은 어디까지나 ‘칠할 수 있는가’라는 판정 문제(Decision Problem)의 이야기입니다. **“실제로 어떻게 4색으로 나누어 칠할 것인가"라는 색칠 알고리즘(Search Problem)**을 구축하는 것은 다른 이야기입니다. 아펠-하켄이나 RSST의 증명 절차를 알고리즘으로 구현하면, 주어진 $N$개의 정점을 가진 평면 그래프에 대해 실제로 4색 칠하기를 구할 수 있는 알고리즘을 얻을 수 있습니다. RSST의 증명에 기반한 알고리즘은 최악의 계산 복잡도 $O(N^2)$의 다항 시간에 4색칠을 출력하는 것으로 나타나 있습니다.

즉, 평면 그래프를 3색으로 칠하려고 하면 우주의 수명만큼 시간이 걸릴지도 모르지만(NP-완전), 4색째를 추가한 순간에 4색 정리 배후에 있는 수학적 구조의 은혜로 고속의($O(N^2)$의) 알고리즘이 존재하게 되는 것입니다. 수학과 컴퓨터 과학이 교차하는, 극히 신비롭고 매력적인 사실입니다.

결론: 4색 정리가 남긴 것

1852년 영국 청년의 소박한 지도 색칠 문제는 단순한 퍼즐로 시작되었습니다. 그러나 그것은 1세기 이상의 시간을 거쳐 그래프 이론이라는 광대한 새로운 수학 분야를 개척했고, 알고리즘 이론을 발전시켰으며, 마침내 “컴퓨터는 수학 증명을 할 수 있는가”, “수학적 진리란 무엇인가"라는 근원적인 철학적 질문을 인류에게 던졌습니다.

4색 정리의 역사는 인간 직관의 한계와 기계라는 새로운 논리 엔진의 가능성이 격렬하게 교차하는 역사입니다. 현재는 케플러의 추측(2014년, 토머스 헤일스의 Flyspeck 프로젝트)이나 페이트-톰프슨 정리 등 다른 거대한 난제들도 정리 증명 지원계를 이용한 형식 검증으로 완전히 증명되었습니다.

우리가 무심코 지도를 4색으로 나누어 칠할 때, 거기에는 오일러의 다면체의 미학과 켐프의 천재적인 좌절, 히우드의 엄밀한 반증, 헤쉬의 방전의 수리, 수천 시간 동안 명멸했던 슈퍼컴퓨터 계산의 궤적, 그리고 Coq의 초준유한사상의 논리가 겹겹이 숨어 있습니다. 4색 정리는 수학이 어떻게 인간의 사고 틀을 넘어 확장해 나가는지를 보여주는 최고의 사례 연구로서 앞으로도 계속 이야기될 것입니다.