7편. 99퍼센트 확신합니다

연재 「당신도 모르는 수학 이야기 ― 수학이란 무엇인가」 · 7편

1611년에 케플러가 얇은 책 한 권을 냈습니다. 새해 선물로 쓴 소책자였고 제목은 「육각형 눈송이」였지요.

그 안에 이런 물음이 있습니다. 크기가 같은 공을 쌓을 때 가장 빽빽하게 쌓는 방법은 무엇인가. 이산기하학에서 가장 오래된 문제입니다. 케플러는 답을 적어 두었습니다. 아래층의 옴폭한 자리에 위층을 얹는 방식, 그러니까 과일 가게에서 오렌지를 쌓는 바로 그 방식이라고요.

증명은 하지 않았어요. 그냥 그렇다고 적어 둔 겁니다.

시작은 대포알이었습니다. 월터 롤리가 조수인 토머스 해리엇에게 갑판에 쌓인 포탄이 몇 개인지 세는 법을 물었고, 그 물음이 돌고 돌아 케플러에게 닿았지요. 1900년에 힐베르트가 스물세 개의 문제를 내놓았을 때 이 물음도 그 안에 들어갔습니다.

풀리기까지 400년 가까이 걸렸습니다. 왜 그렇게 오래 걸렸을까요?

300쪽, 열두 명, 4년

1998년 8월, 토머스 헤일스와 샘 퍼거슨이 증명을 내놓았습니다.

원고는 300쪽이었습니다. 그런데 그 안에 사람이 읽어 낼 수 없는 부분이 있었어요. 헤일스의 증명은 가능한 경우를 하나하나 따져 나가는 방식이었는데, 그 경우가 너무 많아 컴퓨터가 돌려야 했습니다. 논문에는 그 계산을 담은 파일이 함께 딸려 갔고요.

『수학 연보』가 심사를 맡았습니다. 열두 명이 붙었고 4년이 걸렸지요. 논문 하나에 심사위원 열두 명이면 보통 일이 아닙니다.

그리고 이런 답이 돌아왔습니다.

99퍼센트 확신한다.

읽고 나서 한참을 멈췄던 문장입니다. 참이거나 거짓이지, 99퍼센트 참인 정리란 없으니까요. 그런데 심사위원들이 게을렀던 것도 아닙니다. 4년 동안 붙들었고, 확인한 것들은 전부 옳았습니다. 다만 그 계산을 사람이 직접 따라가 확인할 수는 없었어요.

논문은 결국 실렸습니다. 2006년이었으니 제출로부터 여덟 해 만이었지요.

이미 한 번 있었던 일

1976년에도 비슷한 일이 있었습니다.

지도를 칠할 때 네 가지 색이면 충분하다는 명제, 이른바 4색정리가 증명되었을 때입니다. 아펠과 하켄이 존 코크의 도움을 받아 해냈어요.

증명은 이런 모양이었습니다. 어떤 지도든 그 안에 반드시 나타나는 배치를 목록으로 만들고, 그 배치 하나하나가 더 작은 것으로 줄어든다는 것을 보이는 것이지요. 목록에 오른 배치가 1,936가지였습니다. 컴퓨터가 그것들을 하나씩 확인하는 데 천 시간이 넘게 걸렸고요.

논문에는 마이크로필름이 딸려 나갔습니다. 설명과 그림이 450쪽이었어요.

그때 논쟁이 붙었습니다. 사람이 전 과정을 읽어 낼 수 없는 증명을 증명이라 부를 수 있는가.

지금 보면 이상하리만치 현대적인 논쟁이었습니다. 1976년이면 집집마다 컴퓨터가 놓이기 한참 전인데, 그때 이미 물음이 서 있었으니까요.

덧붙이면, 1997년에 다른 수학자들이 배치를 633가지로 줄여 증명을 훨씬 간결하게 만들었습니다. 그래도 컴퓨터가 하는 부분은 사라지지 않았어요.

헤일스가 한 일

99퍼센트라는 말을 듣고 헤일스는 나머지 1퍼센트를 지우기로 합니다.

2003년에 그는 프로젝트를 하나 시작했습니다. 이름은 플라이스펙, 케플러의 형식 증명이라는 뜻을 줄인 말이었지요. 목표는 자기 증명 전체를 기계가 한 줄씩 검사할 수 있는 형태로 다시 쓰는 것이었습니다.

혼자 할 수 있는 일이 아니었습니다. 논문에 이름을 올린 사람만 스물두 명이고, 11년이 걸렸습니다. 2014년 8월 10일에 완료를 알렸어요.

증명 보조기를 두 가지 썼습니다. HOL Light와 Isabelle인데, 각자 잘하는 대목이 달라 나눠 맡겼지요. 그해 10월에 네덜란드 라드바우트 대학에서 다시 검증했는데, CPU 예순 개를 엿새 동안 돌려 9,370 프로세서 시간이 들었습니다. 결과는 같았고요.

그가 그 무렵에 한 말이 오래 남습니다. 이 기술은 수학 심사위원을 검증 과정에서 아예 빼 버린다고, 그러니 그들의 의견은 더 이상 중요하지 않다고요.

가혹하게 들리지만 헤일스 자신이 그 심사에 여덟 해를 바친 사람입니다.

무엇이 증명을 증명으로 만드는가

사람이 쓴 증명은 다른 사람이 읽고 납득해야 정리가 됩니다. 이건 신뢰의 체계예요. 나쁜 체계가 아닙니다. 수학은 이 방식으로 2000년을 굴러왔으니까요. 다만 이 체계는 읽는 사람의 수와 인내심이라는 유한한 것에 묶여 있습니다. 헤일스의 300쪽 앞에서 그 한계가 드러난 것이고요.

형식화된 증명은 다르게 묻습니다. 이 명제가 공리에서 빈틈없이 유도되는가. 그 판정은 기계가 합니다. 심사위원도 학술지도 필요 없고, 이 정도면 명백하다는 문장도 필요 없습니다. 통과하거나 통과하지 않거나 둘뿐이지요.

앞 편에서 우리는 기계가 쓴 증명을 사람이 읽고 만점을 주는 장면을 보았습니다. 여기서는 방향이 반대입니다. 사람이 쓴 증명을 기계가 검사합니다.

두 장면을 나란히 놓으면 이상한 그림이 됩니다. 기계가 쓴 것은 사람이 믿어 주어야 하고, 사람이 쓴 것은 기계가 보증해 주어야 하는 셈이니까요.

그러면 무엇이 증명을 증명으로 만드는 걸까요? 누가 읽었느냐일까요, 아니면 어떤 절차를 통과했느냐일까요?

참고한 것

T. C. Hales, S. P. Ferguson, A proof of the Kepler conjecture, Annals of Mathematics 162 (2005), 1065–1185.

T. Hales 외 21인, A formal proof of the Kepler conjecture, Forum of Mathematics, Pi 5 (2017), e2.

4색정리의 배치 수와 계산 시간은 아펠과 하켄의 1976년 논문 및 그에 관한 후대의 정리를 따랐습니다.