note [🌿 다듬는 중 · growing]

네 색이면 충분하다 — 소설 같은 문제, 소설 같지 않은 증명

발행 2026-08-03 수정 2026-10-08 약 10분 · 각주 2분

목차 7

사회 시간에 받은 백지도에 나라마다 색을 칠한다고 해 보자. 이웃한 나라끼리는 색이 달라야 한다. 색연필은 몇 자루 있어야 할까. 아무리 복잡한 평면 지도라도 네 자루면 충분하다.

여기에는 조건이 두 가지 붙는다. 각 나라는 한 덩어리로 이어져 있어야 하고, 한 점에서만 만나는 나라는 이웃으로 세지 않는다. 두 번째 조건이 왜 필요한지는 피자를 보면 안다. 피자를 여덟 조각으로 자르면 모든 조각이 가운데 한 점에서 만난다. 이것까지 이웃으로 치면 여덟 조각이 전부 서로 이웃이 되어 여덟 색이 필요해진다.

네 색이면 된다는 이 주장이 4색정리다. 네 색을 꼭 다 써야 한다는 뜻은 아니다. 체스판처럼 두 색이면 되는 지도도 있다. 어떤 지도든 네 색이면 칠할 수 있다는 뜻이다. 질문은 초등학생에게도 설명할 수 있다. 답을 증명하는 데는 124년이 걸렸다.

이 문제가 리만 가설 옆에 놓인 글을 종종 본다. 둘 다 “진술은 쉬운데 아무도 못 푸는 문제”로 묶인다. 그런데 4색정리는 미해결이 아니다. 1976년에 풀렸다. 다만 풀린 방식이 난제 이야기의 흔한 결말과 정반대다. 그런 이야기는 보통 천재 한 사람이 칠판 앞에서 마지막 줄을 쓰며 끝난다. 4색정리의 마지막 장면에는 컴퓨터가 있었다.

소설이 좋아할 조건은 거의 다 갖췄다

난제가 이야기 소재가 되려면 몇 가지가 필요하다. 진술이 짧아야 하고, 오래 버텨야 하고, 도전자들의 실패가 쌓여 있어야 한다. 4색정리는 그 조건을 거의 다 채운다.

1852년 프랜시스 거스리(Francis Guthrie)는 잉글랜드의 주 지도를 칠하다가 네 색이면 충분해 보인다는 점을 알아챘다. 그는 수학을 배운 뒤 법학을 공부하던 중이었다. 동생 편에 옛 스승 드모르간에게 질문을 보냈고, 드모르간은 답을 몰라 그날 해밀턴에게 편지를 썼다.¹ 1878년 케일리가 런던 수학회에서 다시 꺼내면서 문제는 더 널리 알려졌다.

질문은 짧았지만, 답을 기다리는 사람들의 명단은 길어졌다.

틀린 증명이 11년 동안 정설이었다

여기까지는 이야기가 순조롭다. 다음 대목은 소설에 나왔다면 작위적이라는 소리를 들었을 것이다.

1879년 알프레드 켐프(Alfred Kempe)가 증명을 발표했다. 수학계는 이를 받아들였다. 11년 뒤인 1890년, 퍼시 히우드(Percy Heawood)가 그 증명에서 구멍을 찾아냈다. 정리는 다시 추측으로 내려갔다.²

같은 일이 한 번 더 일어났다. 1880년 테이트(P. G. Tait)가 또 하나의 증명을 내놓았고, 1891년 페테르센이 그 빈틈을 지적했다.³ 두 번 모두 11년이 걸렸다.

그런데 무너진 증명에도 건질 것이 있었다. 켐프가 쓴 도구인 켐프 사슬(Kempe chain)은 살아남았다. 빨강과 파랑처럼 두 색의 나라만 밟으며 갈 수 있는 데까지 이어지는 한 무리를 찾아, 그 안의 두 색을 통째로 맞바꾸는 기법이다. 이웃들이 네 색을 다 차지해 칠할 색이 없는 나라가 있을 때, 이렇게 색을 맞바꿔 그 나라에 쓸 색 하나를 비워 내려는 것이 켐프의 발상이었다.

맞바꿔도 규칙은 깨지지 않는다. 무리 안에서 맞닿은 두 나라는 원래 빨강과 파랑으로 달랐으니, 함께 뒤바꿔도 여전히 다르다. 무리 바로 바깥의 이웃은 빨강도 파랑도 아니다. 빨강이나 파랑이었다면 무리에 들어 있었을 것이다. 그러니 바뀐 색과 부딪힐 일이 없다.

틀린 증명에서 나온 이 기법은 그 뒤 백 년 동안 이 문제를 공략하는 표준 도구가 됐고, 오늘날의 증명에도 들어 있다. 히우드도 마찬가지다. 그는 켐프의 논증을 부수면서, 그 잔해로 모든 지도는 다섯 색으로 칠할 수 있음을 증명했다.² 문제를 풀지 못한 사람이 문제를 푸는 데 쓰일 부품을 남긴 것이다.

실제 수학이 굴러가는 방식은 이쪽에 가깝다. “천재 한 명이 앉아서 푼다”는 서사에는 잘 담기지 않는 모습이다.

결말은 1,200시간짜리 기계 검사였다

컴퓨터는 정확히 무엇을 검사했을까. 증명의 출발은 의외로 단순하다. 네 색으로 칠할 수 없는 지도, 곧 반례가 있다고 가정한 뒤 그중 나라 수가 가장 적은 지도를 고른다. 이것을 최소 반례라고 부른다.

이제 최소 반례에서 일부를 떼어 낸다. 남은 지도는 가장 작은 반례보다도 작으니 반례일 수 없고, 따라서 네 색으로 칠할 수 있다. 여기에 떼어 낸 부분까지 이어서 칠할 수 있다면 어떻게 될까. 원래 지도도 네 색으로 칠해진다. 반례라고 골랐는데 반례가 아니게 된다.

예를 들어 이웃이 셋 이하인 나라를 떼어 냈다고 하자. 나머지를 칠한 뒤 그 나라를 되돌려 놓으면, 이웃이 쓴 색은 많아야 세 가지라 네 번째 색이 반드시 남는다. 그러니 최소 반례에는 이웃이 셋 이하인 나라가 있을 수 없다.

이렇게 최소 반례 안에는 들어갈 수 없는 작은 패턴을 가약(reducible)이라고 한다. 더 작은 지도로 줄여서 처리할 수 있다는 뜻으로 붙은 이름이다.

이제 할 일을 추리소설에 빗대면 이렇다. 범인이 어느 길로 왔든 적어도 한 곳은 거쳤어야 하는 방들을 빠짐없이 적고, 방마다 범인이 들어갈 수 없었던 이유를 댄다. 수학의 말로 옮기면 필요한 것은 두 가지다.

최소 반례라면 반드시 하나 이상 포함해야 하는 패턴 목록을 만든다.
목록의 패턴이 전부 가약임을 확인한다.

반드시 있어야 하는데 하나도 있을 수 없다. 그러므로 최소 반례도, 반례도 없다. 이것이 증명의 뼈대다.

첫 번째 일인 목록 만들기를 돕는 기법이 헤슈가 발전시킨 방전법이다. 이 기법은 지도를 그래프로 바꿔 다룬다. 그래프는 나라마다 점(꼭짓점)을 하나 찍고, 이웃한 나라끼리 선으로 이은 그림이다. 지하철 노선도가 실제 거리와 모양을 버리고 역과 연결만 남기듯, 그래프도 누가 누구와 이웃인지만 남긴다.

방전법은 꼭짓점마다 숫자를 나눠 주는 데서 시작한다. 돈을 나눠 준다고 생각하면 쉽다. 처음 금액은 꼭짓점마다 이웃 수에 따라 정해지고, 이웃이 많은 꼭짓점은 빚을 안고 시작한다. 그래도 평면 그래프의 점·선·면 개수를 묶어 주는 오일러 공식 덕분에 전체 금액은 반드시 양수가 된다. 그다음 정해 둔 규칙대로 이웃끼리 돈을 주고받게 한다. 주고받기만 하니 전체 금액은 그대로다.

규칙은 다음 성질을 갖도록 짠다. 최소 반례가 될 수 있는 지도에 목록의 패턴이 하나도 없다면, 돈을 주고받은 뒤 모든 꼭짓점이 빈손이거나 빚을 진 상태가 되어야 한다. 전체 금액이 양수라면 누군가는 돈을 쥐고 있어야 하니 앞뒤가 맞지 않는다. 그러니 그런 지도는 존재하지 않는다. 방전이라는 이름은 이 숫자가 전하처럼 옮겨 다닌다고 해서 붙었다.³

걸림돌은 이 반드시 나타나는 패턴 목록, 곧 불가피 집합의 크기였다.

1976년 아펠과 하켄이 증명을 완성했다. 널리 인용되는 목록에는 패턴이 1,476개나 있었고, 컴퓨터 계산에 약 1,200시간이 걸렸다. 계산 작업에는 존 코크도 참여했다.⁴ 경우를 나눠 하나씩 확인하면 된다고 말하기는 쉽다. 하지만 그 경우의 수가 사람이 손으로 검산하기에는 너무 많았다.

1996년 로버트슨·샌더스·시모어·토머스가 같은 전략을 훨씬 단정하게 다시 세웠다. 패턴은 633개로, 방전 규칙은 300개 이상에서 32개로 줄었다. 지도를 실제로 색칠하는 알고리즘도 더 빨라졌다.³ 그래도 전체 경우를 손으로 검산하기는 어려웠다.

2005년 조르주 곤티에는 이 계열의 증명을 증명 보조기 Coq 안에서 형식화했다.⁵ 증명 보조기는 “자명하다”로 건너뛰기를 허락하지 않는 깐깐한 채점자와 비슷하다. 모든 단계가 정해진 논리 규칙에 맞는지 하나하나 확인한 뒤에야 통과시킨다. 곤티에는 계산 절차뿐 아니라, 그 계산이 왜 정리를 증명하는지까지 이 채점자가 검사할 수 있는 형태로 옮겼다.

이때 크게 달라진 것은 무엇을 믿어야 하느냐였다. 개별 검사 프로그램의 결과를 믿는 대신, 증명 보조기의 핵심 검사기인 커널에 논리 검증을 맡긴다. 앞의 채점자 비유로 말하면, 여러 검사 프로그램을 각각 믿고 쓰는 대신, 채점자 한 명에게 공통으로 검사를 맡기는 셈이다. 이 채점자는 다른 수학 증명에도 쓰이므로, 서로 다른 작업을 통해 검사기를 점검할 수 있다.⁵ 물론 정리를 제대로 옮겨 적었는지, 검사기와 실행 환경이 올바른지는 여전히 확인해야 한다. 표현을 바꾼 뒤에도 무엇을 확인해야 하는지는 문제를 옮겨 푼다에서 푸리에 변환과 파일의 해시를 비교하며 살폈다.

계산 증명의 발전은 멈추지 않았다. 2026년 이노우에 등은 꼭짓점이 $n$ 개인 평면 그래프의 색칠 시간을 $O(n^2)$ 에서 $O(n\log n)$ 으로 줄이는 방법을 프리프린트(학술지 심사를 마치기 전에 먼저 공개하는 원고)로 발표했다. $O$ 는 나라 수가 충분히 많아질 때 실행시간의 상한을 잡는 표기다. 앞의 상한은 $n^2$ 의 일정한 배수로, 뒤의 상한은 $n\log n$ 의 일정한 배수로 잡힌다. 나라 수가 아주 많을 때 그 수를 두 배로 늘리면, 이 두 상한식은 각각 네 배와 두 배 남짓으로 커진다. 실제 실행시간이 꼭 그 비율로 늘어난다는 뜻은 아니다. 그런데 이 작업은 오히려 검사할 패턴을 더 많이 쓴다. 목록이 짧아지는 것과 색칠이 빨라지는 것은 다른 개선인 셈이다.⁶

다만 2026년 9월까지 확인한 문헌을 보아도, 널리 받아들여진 증명은 모두 컴퓨터로 경우를 검사하는 방식에 기댄다. 사람이 전체를 손으로 검산할 만한 증명은 여전히 남은 과제다.⁶

평면이 오히려 예외적으로 어렵다

직관을 한 번 더 거스르는 대목이 있다. 지도를 그리는 바탕을 바꾸면 필요한 색 수도 달라지는데, 평면은 그중 색이 가장 적게 드는 바탕이다. 그러니 증명도 가장 쉬울 것 같지만, 실제로는 그렇지 않았다.

지도를 평면 대신 도넛 표면, 곧 토러스 위에 그려 보자. 이때는 일곱 색이면 충분하고, 일곱 색이 꼭 필요한 지도도 있다. 토러스는 구면에 손잡이를 하나 붙인 곡면이다. 머그잔 겉면을 떠올리면 된다. 손잡이를 더 붙여 $g$ 개로 늘릴 수도 있는데, 이 손잡이 수를 종수라고 한다. $g \ge 1$ 인 이런 곡면에서, 모든 지도를 칠하기 위해 준비할 색의 수는

\left\lfloor \frac{7 + \sqrt{48g + 1}}{2} \right\rfloor

이다. 바깥의 꺾인 괄호는 소수점 아래를 버리라는 뜻이다. 손잡이가 1개, 2개, 3개일 때 각각 7색, 8색, 9색이다.

이 공식에는 두 주장이 겹쳐 있다. 색연필이 이만큼이면 어떤 지도든 칠할 수 있다는 상한과, 이보다 적으면 칠할 수 없는 지도가 실제로 있다는 하한이다. 히우드는 상한을 1890년의 그 짧은 논문에서 이미 증명했다. 어려웠던 쪽은 하한이었다. 그런 지도를 종수마다 직접 만들어 보여야 했고, 링겔과 영이 1968년에 이 일을 끝냈다.⁷

손잡이 달린 곡면에서는 이렇게 하한이 더 오래 걸렸다. 구면과 평면에서는 반대였다. 네 색이 꼭 필요하다는 하한은 그림 하나로 끝난다. 가운데 나라 하나를 세 나라가 둘러싸고, 바깥 세 나라도 서로 맞닿게 그리면 네 나라가 모두 서로 이웃이다. 그런데 네 색으로 충분하다는 상한이 124년을 버텼다. 구멍이 없으니 더 쉬울 것 같은데, 정작 마지막까지 남은 것은 구멍 없는 지도였다.

“손으로 증명한다”에 붙는 오해들

이 정리는 픽션과 기사에 자주 불려 나온다. 그때마다 되풀이되는 오해가 몇 가지 있는데, 대부분 손으로 증명한다는 말을 어떻게 이해하느냐에 걸려 있다.

미해결 문제가 아니다. 가장 흔한 착각이다. 밀레니엄 문제 목록에 있는 것도, 아직 답을 모르는 문제도 아니다. 누가 이걸 “푼다”고 할 때 실제로 할 수 있는 일은 셋이다. 기존 증명을 재현하거나, 1996년처럼 계산 증명을 더 단정하게 다시 세우거나, 손으로 검산할 수 있는 새 증명을 내놓는 것이다. 마지막 과제는 아직 남아 있어서, 해낸다면 그 자체로 대사건이다. 그러니 이야기 속 인물이 4색정리를 풀었다고 하면, 셋 중 무엇을 했다는 것인지부터 가려 읽어야 한다.

계산이 빨라진다고 증명이 짧아지지는 않는다. 검사할 경우를 순식간에 확인해도, 사람이 납득해야 할 경우의 수는 그대로다. 손으로 읽을 만한 증명을 원한다면 많은 경우를 한꺼번에 설명하는 아이디어나 더 간결한 증명 구성이 필요하다. 예를 들어 1부터 100까지 더하는 일은 컴퓨터가 눈 깜짝할 새에 끝낸다. 하지만 손으로 쓸 만한 짧은 풀이는 속도에서가 아니라 관찰에서 나온다. 앞뒤 수를 짝지으면(1과 100, 2와 99…) 합이 늘 101이 된다는 관찰이다. 계산 도구가 그런 발견을 도울 수는 있지만, 계산 속도 자체가 설명을 대신해 주지는 않는다.

발표와 인정은 별개의 사건이다. 손으로 쓴 새 증명이 나와도, 다른 사람들이 그 논리를 확인해야 한다. 이 문제에는 한때 받아들여진 증명에서 11년 뒤 오류가 발견된 전력이 있다. 원고 마지막 줄에 마침표를 찍는 장면은 소설의 결말은 될 수 있어도, 그것만으로 수학의 결말이 되지는 않는다.

사람과 컴퓨터를 갈라 세우기도 어렵다. 증명의 전략과 논리는 사람이 만들었고, 컴퓨터는 방대한 패턴 탐색과 검사를 맡았다. 계산 결과는 다시 사람이 목록과 논증을 고치는 데 쓰였다. 사람이 완성한 답에 기계가 마지막에 도장만 찍어 준 것도, 기계가 혼자 아이디어를 낸 것도 아니다. 둘이 주고받으며 완성한 증명이다.

마지막으로, 처음에 붙인 지도 조건을 잊으면 가짜 반례가 생긴다. 본토와 떨어진 영토까지 무조건 같은 색으로 묶으면 네 색으로는 부족한 지도를 만들 수 있다. 한 점에서 만나는 피자 조각을 이웃으로 치는 경우도 마찬가지다. 둘 다 4색정리의 반례가 아니라, 애초에 다른 색칠 문제다.

더 들어가려면

증명 저자들이 직접 쓴 개요: The Four Color Theorem (Robertson–Sanders–Seymour–Thomas)
역사 전반: The four colour theorem (MacTutor)
형식 증명 저장소: rocq-community/fourcolor

프랜시스 거스리는 런던 대학에서 드모르간에게 배웠고, 졸업 후 법학을 공부하던 중 동생 프레더릭 편에 이 질문을 드모르간에게 전했다. 드모르간이 해밀턴에게 편지를 쓴 날짜는 1852년 10월 23일이다. 케일리가 1878년 런던 수학회에서 문제를 다시 제기했다. MacTutor, The four colour theorem. ↩
켐프의 논문은 On the geographical problem of the four colors, American Journal of Mathematics 2 (1879), 193–200이다. 히우드는 1890년 Map colouring theorem에서 오류를 지적하고 5색정리를 보였다. 원 논문 서지는 증명 저자들의 참고문헌, 경위는 MacTutor 참고. ↩ ↩²
패턴 633개, 방전 규칙 32개, 2차 시간 색칠 알고리즘, 그리고 테이트(1880)에 대한 페테르센(1891)의 반박은 Robertson–Sanders–Seymour–Thomas, The Four Color Theorem (Georgia Tech)⁠. 이론적 성과는 1997년에 논문으로 출판됐다. ↩ ↩² ↩³
1,476개는 Robertson–Sanders–Seymour–Thomas의 개요가 비교에 쓰는 아펠–하켄의 목록 크기다. 약 1,200시간의 계산과 코크의 참여는 MacTutor에 나온다. 1976년 증명 발표 뒤 상세 논문은 1977년에 출판됐다. 목록은 이후 수정돼, 모든 판본이 같은 수의 패턴을 쓰는 것은 아니다. ↩
곤티에의 A computer-checked proof of the four colour theorem은 조합적 증명과 평면 지도 사이의 연결까지 형식화한 과정을 설명한다. 2005년에 완료된 작업은 2008년 The Four Colour Theorem: Engineering of a Formal Proof에서도 소개됐다. 코드는 rocq-community/fourcolor에 공개돼 있다. ↩ ↩²
Inoue et al., The Four Color Theorem with Linearly Many Reducible Configurations and Near-Linear Time Coloring, 2026년 프리프린트. 저자들은 $O(n\log n)$ 색칠 알고리즘을 제시하면서, 기존의 올바른 증명들과 자신들의 증명 모두 유한한 경우의 컴퓨터 검사에 의존한다고 설명한다. 본문은 이 알고리즘 결과를 출판된 정설로 단정하지 않고 새 원고의 제안으로 구분했다. ↩ ↩²
여기서는 구면에 손잡이를 붙여 얻는 향가능 곡면만 다룬다. 색 수 공식과 상한·하한의 차이는 Mohar–Thomassen, Graphs on Surfaces, Chapter 8, 1968년 결과는 Ringel–Youngs, Solution of the Heawood map-coloring problem 참고. ↩