|
[ 강연자 소개 ]
컴퓨터 프로그래밍 하기와 수학 문제 풀기를 좋아하던 시골 소년은 군 단위에서는 유일하게 과학고에 갔다가 KAIST를 알게 되어 거기에 진학하였다. 대회 나가면 더 좋은 상을 타오던 컴퓨터 프로그래밍은 그냥 취미로만 하기로 하고, 좀 더 선망하던 수학을 공부하기 위해 수학과를 선택했다. 대학 졸업 후 프로그래머로 회사를 다니다가 수학 공부하러 유학길에 올라 한국인 전공자가 극히 드물던 그래프이론 분야 연구를 하였다. 2008년 모교인 KAIST의 수리과학과 교수로 부임하였고 2012년에는 젊은과학자상을 수상하였다. 이산수학 및 그래프이론 연구 분야는 컴퓨터 알고리듬과 가까워서, 좋아하던 두 가지를 모두 하는 수학자로 지내고 있다.
[ 강연 요약문 ]
컴퓨터와 인터넷이 일상생활의 도구가 된 지금, 수학자들이 하는 증명에는 어떤 변화가 일어나고 있을까? 수학에서 새롭게 나타난 컴퓨터를 활용한 증명을 통해 수학자들이 증명을 인식하는 방법은 어떻게 바뀌었는지 알아본다. 또한 이렇게 복잡한 증명을 수학자 대신 컴퓨터가 증명을 읽고 검증하기도 한다는데 그것이 어떻게 활용되는지 살펴본다. 아울러 인터넷을 통해 수많은 수학자가 동시에 아이디어를 교환하면서 컴퓨터도 일부만 해결한 어려운 수학 문제를 해결한 사례를 보면서 미래 수학 연구가 어떤 모습일지 상상해 보기로 한다.
[ 강연 개요 ]
<컴퓨터를 활용한 증명>
모든 지도는 색깔 4개만 있어도 이웃한 나라가 다른 색이 되도록 칠할 수 있는가? 1852년에 만들어진 이 문제는 4색 문제라고 한다. 무려 120년간 해결되지 않은 난제였으나 1976년 미국 일리오이대학의 아펠과 하켄이 해결하였다. 그러나 전통적인 수학자들과 철학자들은 깊은 고민에 빠졌다. 바로 이 증명은 컴퓨터의 도움을 받아 완성했기 때문이다. 그동안 수학자들은 다른 프로 수학자가 읽고 검증하고 확인할 수 있는 것을 맞는 증명이라고 생각했으나, 수학자가 시킨 대로 컴퓨터가 생성해낸 4색 문제의 증명은 수학자가 다 읽고 손으로 점검하기에는 분량이 너무 많았다. 또한 그 컴퓨터 프로그램의 버그는 없었는지, 그리고 컴퓨터는 한 치의 오류 없이 정상적으로 작동하였을지 의구심을 갖기도 하였다.
오늘날에는 이제 사색 문제의 증명을 대다수 수학자는 받아들이고 있을 뿐 아니라, 컴퓨터 때문에 “증명이란 무엇인가”라는 개념도 바뀌게 되었다는 것을 인정하게 되었다.
지름이 같은 공을 최대한 조밀하게 쌓으면 얼마나 채울 수 있을까? 17세기 케플러는 우리가 시장에서 사과를 쌓는 방법으로 하면 최적이지 않겠는가 질문하였다. 하지만 무려 똑같지 않겠는가 질문을 하였다. 이 케플러 추측은 400년간 미해결 문제였으나, 1998년 미국의 수학자 헤일스가 이 것을 증명하였다고 발표하였다. 이 증명은 검증을 거쳐 2005년 수학계의 최고 저널인 수학연보에 출판되었다. 그러나 저널의 편집자들과 심사자들은 이 증명이 100% 맞다는 확신을 할 수 없었다. 4년간 무려 12명의 심사자가 이 논문에 매달렸으나 99% 맞다는 확신밖에 할 수 없었다고 했다는데, 그 이유는 바로 헤일스의 증명 역시 모든 경우를 따져 최적을 계산하는 것인데, 각각의 경우를 복잡한 컴퓨터 계산으로 해결하였기 때문이다. 이것을 검증하는데 사용한 프로그램에 오류가 정말 하나도 없었을까?
<컴퓨터가 검증하는 증명>
인간이 다 읽고 검증할 수 없는 분량의 연구라면 증명이 맞고 틀린 것을 독립적으로 확인할 방법은 없을까? 최근에는 수학자 대신 컴퓨터 프로그램이 증명을 읽고 검증할 수 있도록 하는 연구가 진행되고 있다. 참이라고 인정하는 공리를 입력해두고 거기서부터 논리적으로 모든 것을 유도해서 증명의 모든 과정이 정확하게 논리적으로 증명되는지 확인하는 소프트웨어가 여럿 나왔다. 이를 사용하여 2005년에 영국의 마이크로소프트 연구소의 곤띠에는 컴퓨터가 검증할 수 있는 증명을 통해 4색 정리를 증명하였다. 2014년에는 헤일스의 증명 역시 컴퓨터가 검증할 수 있는 증명으로 새로 작성되어 컴퓨터로 검증되었고 2017년에 그 검증과정을 담은 논문이 출판되었다. 이제는 검증하는 컴퓨터 프로그램과 그 프로그램이 가정하는 공리만 믿으면 위 증명은 수학적으로 엄밀하게 맞다고 확신할 수 있을 것 같다.
이러한 증명 검증용 컴퓨터 프로그램은 어떻게 활용될까? 수학적으로 엄밀하게 무엇인가를 증명하고자 하는 경우가 수학 바깥에도 많이 있다. 실제로 이러한 증명 검증용 프로그램은 컴퓨터 프로그램나 CPU 설계에서 오류가 하나도 없는지 확인하고 검증하는데 활용되며, 또한 중요한 암호 프로그램 설계에서 보안 오류가 발생하지 않는지 엄밀하게 검증하는데 활용된다.
<수학자들의 희망 스토리? 인터넷을 통한 공동연구 폴리매쓰 프로젝트>
과연 4색 문제나 케플러 추측처럼 컴퓨터 힘을 빌려서만 해냈던 증명은 언젠가는 사람의 손으로 검증할 수 있는 새로운 증명이 나올 수 있을까요?
1930년대 헝가리의 유명한 수학자인 에르되시는 +1, -1을 무한히 많이 늘어놓더라도 모든 C에 대하여 적당히 처음부터 같은 간격으로 뛰어넘고 만나는 수를 더해나가면 그 합의 절댓값이 C 이상이 되는 순간이 반드시 존재하지 않겠는가 질문을 하였다. 이 질문은 무려 80년 이상 미해결문제였다. C=3인 경우에 이 질문이 맞다는 것이 2014년에 영국의 두 수학자에 의해 증명되었는데 당시 이 증명은 수학 역사상 가장 “용량이 큰” 증명이었다. 그 당시 증명은 무려 컴퓨터 파일로 13기가바이트였다. 이들 역시 컴퓨터를 사용하였는데, +1, -1을 합쳐서 총 1161개를 어떻게 적더라도 반드시 C=3일 때 참이 되도록 한다는 것을 컴퓨터 프로그램(3-SAT solver)을 통해 증명하였다. 아직도 C=4일때는 +1, -1을 얼마나 많이 쓰면 반드시 C=4 이상이 되는지는 누구도 알지 못하고 있다.
하지만 2015년 미국 ULCA의 유명한 수학자 테렌스 타오는 모든 C에 대해 에르되시의 저 문제가 참이라는 것을 증명하였다. 이 새로운 증명은 13기가바이트의 자료도 필요없고 사람의 힘으로 검증가능한 분량이었다.
이러한 결과가 나오기까지는 그 전에 “폴리매쓰 프로젝트”라고 불리는 협업 프로젝트의 도움이 컸다. 폴리매쓰는 인터넷에서 수많은 수학자들이 함께 아이디어를 공유하면서 하나의 문제를 풀기 위해 도전하는 과정인데 폴리매쓰 프로젝트 중 5번째 프로젝트가 바로 에르되시의 이 문제였고, 폴리매쓰 프로젝트에서 이 문제를 풀지는 못하였지만 푸는데 결정적으로 필요했던 아이디어인, 이 수열이 특정한 성질을 만족하는 경우에만 보면 된다는 것을 증명하였다. 테렌스 타오 교수는 이 성질을 만족하는 경우에 어떻게 되는지 분석하여 에르되시의 추측의 증명을 완성할 수 있었다. 이 문제는 컴퓨터 계산으로는 조금밖에 할 수 없는 것도 인간들의 협업으로 해낼 수 있다는 것을 보여줬다.
|
