d라이브러리

4색 정리는 컴퓨터로 해결한 대표적인 수학 문제입니다. 컴퓨터의 손을 빌린 만큼 증명 과정도 너무 길어서 다 읽고 확인한 사람이 없지요. 결국 검증도 컴퓨터의 도움을 받고 말았습니다. 4색 정리의 응용문제 역시 2016년 컴퓨터의 도움으로 해결했는데요, 최근 덴마크 수학자가 기발한 아이디어로 컴퓨터를 쓰지 않고 이 문제를 풀었습니다.

그러던 2016년 4월 스티븐 하케 미국 콜로라도 덴버대학교 교수와 브렌트 토마스 박사, 소골 야한베캄 미국 로체스터공과대학교 교수가 컴퓨터를 이용해 문제를 풀었다고 밝혔습니다. 연구팀은 4색 정리를 해결할 때 사용했던 기술을 적용해 베크너의 문제를 증명했습니다.

1976년 미국 수학자 케네스 아펠과 볼프강 하켄은 4색 정리 증명을 위해 귀류법을 사용합니다. 4색 정리가 틀렸다고 가정하고 모순을 이끌어 내지요. 즉 4색 정리에 반례가 있다면 반드시 반례인 1936개 경우 중 하나가 되는데, 그 경우도 4색이면 충분히 색칠할 수 있다는 걸 보여 4색 정리를 증명했습니다. 그 중에서도 최소 행정구역의 수를 가진 반례에 대해서는 1936개 경우에 속하지 않기 때문에 4색으로 칠할 수 있다고 증명하지요.

연구팀은 이 방법을 그대로 따와 증명합니다. 그런데 그 경우의 수는 확 줄었습니다. 사용한 색의 수가 많다보니 1936개 경우를 31개로 줄일 수 있었습니다. 먼저 베크너의 문제에 반례가 있다면 31개 중 하나를 반드시 포함한다는 걸 컴퓨터의 도움 없이 보입니다. 이후 최소 행정구역 수를 가진 반례는 31개 경우 각각을 포함할 수 없다는 걸 컴퓨터로 일일이 따져 증명합니다. 그 중 어떤 부분은 인텔 제온 CPU 48개를 사용해 55일간 계산했습니다.

비로소 성공한 토마센 교수

그런데 2017년 8월 토마센 교수가 인터넷에 베크너의 문제를 푼 논문을 공개합니다. 이번엔 학술지 ‘조합적 이론 시리즈 B’의 게재 승인까지 받았다고 밝혔습니다. 여러 수학자의 검증 과정을 거쳤으니 문제가 풀렸다고 볼 수 있겠지요?

이 논문은 앞서 소개한 것과 다르게 컴퓨터를 전혀 쓰지 않았습니다. 다만 훨씬 더 복잡하지요. 제가 보기에도 어려우니 검증하기가 만만하지 않았을 겁니다. 하지만 증명 아이디어는 상당히 재밌습니다.

일단 다음 조건이 되도록 행정구역들을 둘로 잘 나눕니다. 둘로 나눈 것 중 하나를 빨간색 행정구역, 다른 하나를 파란색 행정구역이라고 합시다. 먼저 빨간색 행정구역끼리 서로 거리 2 이내인 것을 모아서 보면 4색 정리가 된다는 것을 보입니다. 그러면 빨간색 부분은 모두 4색으로 칠해지겠지요? 그 다음 파란색 행정구역끼리 서로 거리 2 이내인 것들을 보면 3색 이하로 칠 해진다는 것을 보입니다. 그럼 총 7색만 사용해서 지도가 칠해집니다.

베크너의 문제는 컴퓨터를 쓴 증명이 나온 직후에 컴퓨터를 쓰지 않은 증명이 나온 아주 특이한 경우입니다. 4색 정리도 베크너의 문제처럼 기발한 아이디어로 컴퓨터를 쓰지 않고 풀 수 있을까요? 100년 뒤로 이동하는 타임머신이 있다면 가서 물어보고 싶습니다.