[테크홀릭] 지난 1611년 독일 천문학자이자 수학자, 점성술사이기도 했던 케플러(Johannes Kepler. 사진 위)는 “상자 안에 가장 효율적으로 (오렌지 같은) 구체를 쌓는 방법은 과일가게가 가게 앞에 오렌지를 쌓는 것과 같은 방법”이라는 추측을 했다. 얼핏 쉬워 보이는 이 명제를 증명하는 데 걸린 시간은 무려 400년이다. 기간으로는 수학자를 괴롭힌 난제였던 페르마의 마지막 정리와 맞먹는 기간이 걸린 것이다.
그의 추정은 구체를 쌓아올리는 데 가장 좋은 방법에 대한 것이다. 그는 가장 효과적인 방법으로 과일가게가 오렌지를 쌓는 것 같은 피라미드식 누적이라고 설명했다. 그런데 이 추정은 지금까지 증명되지 않았었다. 이 케플러의 추정을 증명한 건 미국 피츠버그대학 토마스 헤일스(Thomas Hales) 박사다.
그가 케플러의 추정을 증명한 건 지난 1998년이다. 구체를 쌓아 올리는 방법은 무궁무진하지만 대부분은 수천 가지의 방법에서 변형한 것이다. 그는 구체를 쌓는 방법을 수학적으로 표현할 수 있는 수천 가지로 분류한 다음 소프트웨어를 이용해 조사했다. 증명은 300페이지에 달하는 방대한 양이어서 비평가 12명이 매달려 4년에 걸쳐 확인했고 지난 2005년 수학연보(Annals of Mathematics)에 99% 확률로 올바른 것으로 발표했다.
2003년 헤일스 박사 연구팀은 플라이스펙(Flyspeck)이라는 프로젝트를 시작했다. 이미 정확도 99%로 케플러의 추정을 입증했지만 연구팀은 작은 오류까지 확인할 수 있는 커널을 갖춘 프로그램을 이용해 증명이 옳다는 것을 체크했다.
32코어 병렬 처리 시스템을 이용해 정답 맞추기에 들어간 것이다. 이 검증에 이용한 프로그램은 존 해리슨(John Harrison)이 개발한 HOL 라이트(HOL Light)와 이사벨(Isabelle)이다. 이 프로그램은 일련의 수학적 증명에 대환 정확도를 확인할 수 있도록 설계되어 있다. 이 과정을 거쳐 올해 8월 10일 연구팀은 헤일스 박사의 증명을 컴퓨터로 분석한 결과 맞았다는 발표를 한 것이다.
헤일스 박사는 기술은 인간이 수학적 증명의 정확성을 평가할 필요가 없어지게 만들었다면서 앞으로 많은 수학자의 증명 정확도를 평가하는 데 컴퓨터가 쓰이게 될 것이라고 밝혔다. 세계적인 수학자가 컴퓨터를 이용해 자신의 증명을 검증했다는 것 자체가 의미 있는 케이스 스터디가 될 것이라는 설명이다. 관련 내용은 이곳에서 확인할 수 있다.
전자신문인터넷 테크홀릭팀
이상우 기자 techholic@etnews.com