지금 이곳에선 2018년 필즈상 수상자인 페터 숄체 독일 본대학교 교수님의 증명을 검증하고 있어. 심사위원은 바로 나! ‘LEAN(린)’이야. 소프트웨어(SW)가 지구 최고 수학자의 증명을 검증한다니 놀랍지?
[계산이 복잡할 땐 나를 불러! 린]
후우~. 검증이 끝나고 바로 달려왔어. 놀라지 마! 내가 숄체 교수님의 연구에서 오류를 발견했다고. 교수님도 깜짝 놀랐어. 내가 어떤 일을 했는지 지금 바로 공개하지!
수학계의 스타! 숄체 교수님은 2018년, 도형을 모양보다는 위치와 구멍의 개수로 분류하는 ‘위상수학’에 새로운 개념을 도입하면 수의 성질을 연구하는 정수론 문제에 유용한 도구를 제공할 수 있을 거라 생각했어. 그리고 더스틴 클라우센 덴마크 코펜하겐대학교 수학과 교수님과 함께 이런 내용을 연구하는 새로운 수학 분야를 만들고 ‘콘덴스드 수학(Condensed Mathematics)’이라고 이름 붙였지. 이 분야의 목표는 공간과 함수를 연구하는 ‘위상수학’과 ‘해석학’에서 기존에 사용하던 ‘위상 공간’ 대신 새롭게 정의한 ‘콘덴스드 집합’을 사용해 다시 쓰는 거야. 이렇게 하면 정수론 연구에 유용한 도구들이 생기게 되고, 해석학과 해석기하학마저도 대수학으로 편입시킬 수 있는 혁신적 도전이지. 여기서 대수학은 수학 구조를 연구하는 분야야.
숄체 교수님은 이 분야의 기초를 정립하기 위해 ‘형식 증명’을 해 나갔어. 형식 증명이란 증명 과정에서 생기는 명제의 의미를 고려하지 않고 미리 정의한 공리와 명제가 참이라 가정한 뒤 형식적으로 증명하는 걸 말해. 이 방법을 사용해 여러 추측을 만들었는데, 그중 한 추측을 ‘액체 텐서 실험’이라 이름 붙이고 증명하고자 했어. 숄체 교수님이 “지금까지 내가 찾은 것 중 가장 중요한 추측이라고 생각한다”고 케빈 버자드 영국 임페리얼칼리지런던 교수님의 블로그에 밝힐 정도로 의미 있는 추측이야.
복잡하고 많은 계산량, 린이 검증!
피나는 노력 끝에 숄체 교수님은 2019년 7월 추측을 증명했지. 하지만 증명 과정 속 엄청난 양의 계산 때문에 이 계산이 다 맞다는 확신이 없었어. 작은 실수가 있을 수도 있다 생각했지만 많은 계산을 또다시 해보는 것은 엄두가 나지 않았지. 숄체 교수님은 버자드 교수님의 블로그를 통해 “2019년 내내 이 추측의 증명에 사로잡혀 거의 미칠 뻔했다”고 말했어.
그때 숄체 교수님은 증명 보조 SW인 나를 떠올린 거야! 그리고 나를 활용해 자신의 증명을 검증하기로 마음먹고 ‘린 전도자’로 유명한 버자드 교수님에게 연락했어. 버자드 교수님과 숄체 교수님은 자신이 연구하는 내용을 내 팬 사이트(린 커뮤니티) 구성원에게 공유했지. 숄체 교수님의 연구에 참여하고 싶었던 수학자들은 내가 이해할 수 있는 언어로 교수님의 증명에 필요한 정리와 정의 등을 입력해 줬어. 그렇게 모든 정보를 입력하고 내가 계산을 끝마치는 데 약 5개월이 걸렸어.
그 결과 내가 숄체 교수님의 계산 실수도 잡아냈지! 뭐, 증명에는 크게 영향을 미치진 않았지만 말이야. 숄체 교수님은 “이번 실험은 린이 얼마나 유능한지에 대한 나의 생각을 확 바꿨다”고 버자드 교수님의 블로그에서 말했어!
[컴퓨터와 수학자가 함께하는 미래는?]
내가 어떤 연구를 검증했는지 알고 나니 나에 대해 더 궁금하지? 그리고 다른 수학자들은 날 어떻게 활용하는지 궁금할 거야. 지금 바로 알려 줄게.
난 2013년 마이크로소프트 리서치 팀의 레오나르도 드모라가 개발한 수학 증명 보조 SW야. 내가 수학 증명을 검증하기 위해선 수학자가 수학의 가장 기본적인 정의부터 복잡한 정의까지 내가 이해할 수 있는 언어로 바꿔서 입력해 줘야 해. 나는 수학자가 입력한 정의를 토대로 검증하기 때문에 검증에 필요한 자료가 없으면 검증을 할 수 없어. 그래서 자료가 충분히 쌓이지 않은 과거에는 검증 도우미의 역할보단 디지털 수학 도서관의 역할을 많이 했어.
내가 작동하기 위해선 수학 지식 저장소인 ‘매스 라이브러리’가 꼭 필요해. 매스 라이브러리엔 검증을 통과한 수학 정의와 정리들이 모여 있지. 내 팬 사이트(린 커뮤니티)에 들어가면 증명을 SW 언어로 입력하는 방법을 볼 수 있어. 방법을 익히면 누구나 증명을 등록할 수 있지. 하지만 등록한다고 해서 모든 증명이 매스 라이브러리에 저장되는 것은 아니야. 내가 검증하거나, 인간 관리자의 검토를 거쳐 참인 증명만 등록되거든.
점점 똑똑해지는 SW 린!
2019년 숄체 교수님이 증명의 검증을 내게 부탁했다는 사실이 수학계에 소문나면서 나를 향한 수학자들의 관심이 쏟아졌어. 내가 수학 연구에 도움을 줄 수 있다는 확신을 갖기 시작했거든. 실제로 내 저장소인 매스 라이브러리에 저장된 정의와 정리가 2020년 10월에는 각각 1만 8,416개, 3만 8,315개였는데 약 1년 만에 두 배 가까이 늘어서 2022년 1월 3일 기준으로 3만 441개의 정의와 7만 3,011개의 정리가 저장됐어. 엄청나지? 이 속도라면 더 많은 수학자의 증명을 검증할 수 있을 것 같아!
앞으로 더 많은 수학자가 나를 사용하면 더 많은 내용이 쌓여 대부분의 증명을 검증할 수 있을지도 몰라. 또 수학자를 돕는 AI의 활약도 계속될 거고. 더 발전할 일만 남은 컴퓨터와 수학자의 협업! 2022년에는 또 어떤 흥미롭고 엄청난 연구를 수학자와 함께할지 기다려진다! 너희들도 내 활약을 지켜봐 줘~.
_ 인터뷰
수학자와 컴퓨터의 연결 고리를 만드는 수학자
나를 숄체 교수님께 소개한 케빈 버자드 교수님은 2022년 세계수학자대회의 기조 강연자로도 초청받았어. 과연 버자드 교수님이 생각하는 수학자와 컴퓨터의 협업은 어디까지일까?
Q 수학 연구에서 AI를 포함한 컴퓨터가 아직 할 수 없는 영역은 무엇인가요?
컴퓨터 스스로 기발한 아이디어를 내는 부분입니다. 컴퓨터는 1초에 수백만 개의 아이디어를 떠올릴 순 있지만, 그 아이디어 중 어느 것이 뛰어난지 스스로 파악하기는 어려워요. 또 방정식을 사용하는 대수학은 쉽게 익히지만, 다양한 도형을 그려야 하는 기하학 분야는 습득하기 쉽지 않습니다.
Q 컴퓨터가 수학자를 대체할 수 있을까요?
아직 어렵다고 봅니다! 많은 인공지능 연구가 이를 실현하기 위해 노력하고 있지만 현재로선 가까이 오지도 못했습니다. 수학자를 아주 잘 돕는 컴퓨터를 기대하는 것이 더 현실적인 목표라고 생각합니다. 바둑에서 AI가 인간을 이겼다고 해서 바둑 기사가 사라지진 않았잖아요. 오히려 AI 덕분에 바둑을 더 잘 이해하게 됐지요. 때문에 수학자만큼 수학을 잘하는 AI가 등장해도 수학자를 대체할 순 없습니다.
Q 수학자와 컴퓨터의 협업은 어디까지일 거라 예상하세요?
미래에는 컴퓨터가 수학 전반에 걸쳐 인간을 도울 것이라 기대해요. 하지만 앞으로 10년 동안은 인간이 수학에서 컴퓨터보다 더 많이 활약할 거라 생각합니다. 당분간 컴퓨터는 새로운 정리를 증명할 때 도움을 주는 작은 역할만 할 겁니다.
Q 현재는 어떤 연구를 하고 있나요?
최근 컴퓨터가 숄체 교수님의 증명처럼 매우 어려운 내용을 이해하는 데 한 번 성공했지만, 아직 컴퓨터가 질문을 이해하지 못하는 경우가 더 많이 있습니다. 지금 제 연구의 많은 부분이 이것을 정리하는 데 집중돼 있어요. 일단 컴퓨터가 다양한 질문을 이해하면, 그때가 바로 정답에 대해 생각하기 시작할 때입니다. 그날을 위해 아직 해야 할 일이 많습니다.
