note [🌿 다듬는 중 · growing]

네 색이면 충분하다 — 소설이 쓸 수 없는 방식으로 풀린 문제

약 6분 · 각주 2분

이 글의 출발점 《전능의 뇌를 얻었다》

목차 7

지도를 색칠할 때 국경을 맞댄 두 나라가 같은 색이 되지 않게 하려면 몇 가지 색이 필요한가. 답은 넷이다. 이 문장은 초등학생에게도 설명할 수 있고, 실제로 1852년에 잉글랜드 지도를 색칠하던 학생이 발견했다.1

이 문제가 리만 가설 옆에 놓인 글을 종종 본다. 둘 다 “진술은 쉬운데 아무도 못 푸는 문제”로 묶인다. 그런데 4색정리는 미해결이 아니다. 1976년에 풀렸다. 다만 풀린 방식이, 난제를 다루는 이야기가 보통 고르는 결말과 정반대다.

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

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

진술에는 예비지식이 필요 없다. 1852년 프랜시스 거스리(Francis Guthrie)가 이 문제를 떠올렸을 때 그는 런던 대학에서 드모르간에게 배운 뒤 법학을 공부하던 중이었고, 동생을 통해 옛 스승에게 질문을 전달했다. 드모르간은 답하지 못했고, 질문을 받은 그날 해밀턴에게 편지를 썼다.1 1878년 케일리가 런던 수학회에서 이 문제를 다시 꺼내면서 본격적인 공격이 시작됐다.

그리고 124년을 버텼다. 1852년에서 1976년까지다.

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

여기까지는 이야기가 잘 굴러간다. 다음 대목은 소설이 지어냈다면 작위적이라고 할 만하다.

1879년 알프레드 켐프(Alfred Kempe)가 Nature에 증명을 발표했다. 받아들여졌다. 11년 뒤인 1890년, 퍼시 히우드(Percy Heawood)가 그 증명에 결함이 있음을 보였다. 정리는 다시 추측으로 내려갔다.2

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

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

이게 실제 수학이 굴러가는 방식에 가깝다. 그리고 “천재 한 명이 앉아서 푼다”는 서사가 잘 담지 못하는 부분이기도 하다.

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

20세기의 진전은 두 개의 아이디어 위에 쌓였다. 하나는 버코프의 가약성(reducibility)이다 — 어떤 국소 패턴은 최소 반례 안에 있을 수 없다. 다른 하나는 1969년 헤슈가 정리한 방전법(discharging)으로, 오일러 공식에서 정점과 면에 ‘전하’를 매긴 뒤 재분배해 그런 패턴이 어딘가 반드시 나타남을 강제하는 기법이다.

둘을 합치면 증명의 뼈대가 나온다. 반드시 나타나는 패턴들의 목록 — 불가피 집합(unavoidable set) — 을 만들고, 그 목록의 모든 원소가 가약임을 보인다. 문제는 그 목록의 크기였다.

1976년 아펠과 하켄이 목록을 완성했다. 최종 불가피 집합은 configuration 1,476개였고(초기 목록은 1,936개), 가약성 검사에 1,200시간이 넘는 계산이 들었다.4 사람이 손으로 검산할 수 있는 분량이 아니다.

1996년 로버트슨·샌더스·시모어·토머스가 같은 전략을 훨씬 단정하게 다시 세웠다. configuration은 633개로, 방전 규칙은 300개 이상에서 32개로 줄었고, 색칠 알고리즘도 4차에서 2차로 내려갔다.3 그래도 여전히 손으로는 못 읽는다.

2005년 조르주 곤티에가 이 증명 전체를 증명 보조기 Coq 안에서 형식화했다.5 이때 바뀐 것은 증명의 내용이 아니라 믿어야 할 대상이다. 여러 개의 검사 프로그램이 옳게 짜였다는 믿음이, 증명 보조기 커널 하나가 옳다는 믿음으로 옮겨 갔다. 이 이동 자체는 문제는 풀리지 않는다, 옮겨질 뿐에서 따로 다뤘다.

문제가 제기된 지 170년이 넘었지만, 수학계가 받아들인 손 검산 가능한 증명은 아직 없다.6

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

직관을 한 번 더 거스르는 대목이 있다. 평면이 가장 쉬운 경우일 것 같지만, 색칠 문제에서는 그렇지 않다.

도넛 표면(토러스)에서는 일곱 색이 필요하다. 종수 gg인 향가능 곡면 일반으로 가면 필요한 색의 수는

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

이고, g=1,2,3,…g = 1, 2, 3, \dots에 대해 7, 8, 9, …로 이어진다. 히우드는 이 공식의 상한을 1890년의 그 짧은 논문에서 이미 증명했다. 어려웠던 쪽은 하한 — 그만큼의 색이 실제로 필요한 곡면 분할을 종수마다 구성하는 일이었고, 링겔과 영이 1968년에 끝냈다.7

즉 고차 종수에서는 상한이 쉽고 하한이 어렵다. 구면과 평면은 정확히 반대다. 하한(네 색이 필요한 지도)은 그림 하나로 끝나는데, 상한(네 색으로 충분하다)이 124년을 버텼다. 평면은 이 계열에서 가장 쉬운 경우가 아니라, 나머지와 논증 구조가 뒤집힌 예외다.

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

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

미해결 문제가 아니다. 가장 흔한 미끄러짐이다. 밀레니엄 문제 목록에 있지도 않고 열려 있지도 않다. 누가 이걸 “푼다”고 할 때 실제로 가능한 일은 기존 증명의 재현이거나, 1996년처럼 계산 증명을 더 단정하게 다시 세우는 일이거나, 손 검산 가능한 새 증명이다. 마지막 쪽은 지금도 비어 있는 칸이니 그 자체로 대사건이지만, 이야기는 대개 그 구분을 하지 않는다.

압축에 필요한 것은 계산력이 아니다. 633개까지 줄이는 데 아펠–하켄 이후 20년이 걸렸고, 그러고도 여전히 손으로는 못 읽는다. 여기서 더 줄이려면 새로운 구조 원리 — 그 모든 경우를 몇 개의 강한 명제로 눌러 담을 좌표계 — 가 있어야 하는데, 그런 것이 존재한다는 보장조차 없다. 아무리 빠른 머리를 가정해도 이 벽은 그대로다. 부족한 것이 속도가 아니라 형태이기 때문이다.

증명이 나온 다음이 더 길다. 손으로 쓴 4색정리 증명이 나온다면 학계의 첫 반응은 환호가 아니라 검증일 것이고, 그 검증에는 사람이 붙어야 하며, 이 문제는 이미 두 번, 검증을 통과했다가 뒤집힌 전력이 있다. 발표 직후에 곧바로 인정받는 전개가 이 문제의 실제 역사와 가장 어긋난다.

컴퓨터가 푼 것이 아니다. 손 증명을 대비항으로 놓을 때 따라오기 쉬운 오해다. 기계가 한 일은 사람이 설계한 구조 안에서 유한한 경우들을 검사한 것이고, 무엇을 검사할지 — 불가피 집합의 설계 — 는 사람 쪽이었다. “컴퓨터 대 사람”이 아니라 “설계는 사람, 검산은 기계”다.

덧붙여 지도 자체를 그릴 때의 주의점 하나. 정리가 성립하려면 각 나라가 하나로 이어져 있어야 한다. 본토와 떨어진 영토를 같은 색으로 칠해야 한다면 네 색으로는 부족해진다.8 실제 세계지도가 반례처럼 보이는 이유가 대개 이것이다.

더 들어가려면

주석

  1. 프랜시스 거스리는 런던 대학에서 드모르간에게 배웠고, 졸업 후 법학을 공부하던 중 동생 프레더릭을 통해 이 질문을 드모르간에게 전했다. 드모르간이 해밀턴에게 편지를 쓴 날짜는 1852년 10월 23일이다. 케일리가 1878년 런던 수학회에서 문제를 다시 제기했다. MacTutor, The four colour theorem. ↩ ↩2

  2. 켐프의 증명은 1879년 Nature에 실렸고, 히우드가 1890년 논문 Map colouring theorem에서 결함을 보였다. 같은 논문에서 5색 정리가 증명됐다. 켐프 사슬은 그의 실패한 증명에서 나온 기법이다. MacTutor, The four colour theorem. ↩ ↩2

  3. configuration 633개, 방전 규칙 32개, 2차 시간 색칠 알고리즘, 그리고 테이트(1880)에 대한 페테르센(1891)의 반박은 Robertson–Sanders–Seymour–Thomas, The Four Color Theorem (Georgia Tech). 이론적 성과는 1997년에 논문으로 출판됐다. ↩ ↩2

  4. 1,476개 configuration과 1,200시간 이상의 계산은 널리 인용되는 수치다. 초기 불가피 집합이 1,936개였다가 축소된 경위를 포함해 MacTutor와 Robertson–Sanders–Seymour–Thomas의 개요가 서로 다른 시점의 숫자를 인용하고 있어, 자료마다 1,476~1,936 사이로 갈린다. 아펠·하켄의 작업에는 대학원생 존 코크가 함께했다. ↩

  5. 곤티에의 형식화는 2005년에 완료됐고 2008년에 발표됐다. 저장소는 현재 Coq/Rocq 커뮤니티에서 이브 베르토가 관리하며, 실수 공리계·평면 위상·조합적 hypermap 이론까지 함께 담고 있다. rocq-community/fourcolor, Gonthier, The Four Colour Theorem: Engineering of a Formal Proof. ↩

  6. 짧고 사람이 검산할 수 있는 증명을 주장하는 원고는 꾸준히 나온다. 예를 들어 arXiv:1708.07442, A Human-Checkable Four-Color Theorem Proof가 있다. 이런 원고들이 동료 심사를 통과해 표준 증명으로 자리 잡았다는 근거는 확인하지 못했다. 증명 저자들과 형식화 저장소가 여전히 아펠–하켄 계열의 계산 증명을 표준으로 서술한다. ↩

  7. 히우드 추측은 1890년에 제기되어 1968년 링겔과 영이 해결했다. 종수 0, 1, 2, 3, …에 대해 4, 7, 8, 9, …가 되며, 종수 0(구면)은 공식이 4를 주지만 증명의 난이도 구조가 나머지와 반대인 예외다. 클라인 병도 예외로, 공식의 7이 아니라 6이다. Heawood conjecture, Ringel–Youngs, Solution of the Heawood map-coloring problem, PNAS 60(2). ↩

  8. 정리의 표준 진술은 각 영역이 연결된(단일 조각인) 평면 지도를 전제한다. 비연결 영역을 한 색으로 강제하면 필요한 색의 수에 상한이 없어진다. ↩