수학 초지능과 형식 증명: AI가 만든 증명의 검증 병목을 Lean과 Mathlib으로 푸는 법

핵심 메시지

• 수학은 4천 년 동안 사람이 증명을 쓰고 동료가 읽어 확인하는 신뢰 기반 절차로 굴러왔지만, 그 절차가 한계에 다다랐다.
• AI는 불과 2년 만에 고교 경시 수준에서 국제수학올림피아드 상위권 수준으로 올라섰고, AI가 네 시간 만에 만든 증명을 사람 전문가는 한 시간씩 붙잡고 검토해야 한다.
• 그런 증명을 검토할 능력이 있는 수학자는 전 세계에 수천 명뿐이고 이들에게는 이미 본업이 있어, 사람이 곧 발견의 병목이 된다.
• 대안은 사람의 언어 대신 기계가 검사할 수 있는 언어로 증명을 쓰는 형식 수학이며, 증명 보조 언어 Lean과 약 200만 줄 규모의 정리 라이브러리 Mathlib이 그 토대다.
• 올해 국제수학올림피아드에서 자동화 시스템이 6문제 중 5문제를 사람의 검토가 전혀 필요 없는 형태로 풀어 금메달급 성적을 냈다.

쉽게 이해하기

강연은 4천 년 된 바빌로니아 점토판에서 시작한다. 이차방정식의 선조 격인 이 기록 이후 수학은 줄곧 같은 방식으로 굴러왔는데, 누군가 아이디어를 적으면 동료들이 읽고 따져 확인하는 창의성과 소통과 신뢰의 절차다. 물리학자 유진 위그너의 표현을 빌리면 이 방식은 '터무니없이 효과적'이었다.

그 효과는 오늘의 기술 전부에 남아 있다. 19세기에 사고 실험으로 출발한 비유클리드 기하는 일반상대성이 필요로 한 바로 그 수학이 됐고, 대칭을 다루려 만든 군론은 입자물리와 결정 구조의 언어가 됐으며, 가장 순수해서 쓸모없다 여겨지던 정수론은 지금 온라인에서 오가는 수조 달러를 지킨다. 강연자는 현대 AI 역시 신경망이라는 거대한 응용 수학 구조물이며, 학습이란 수십억 차원의 공간을 미적분의 도구로 항해하는 일이라고 정리한다.

문제는 검증 비용이다. 2002년 그리고리 페렐만은 푸앵카레 추측에 대한 짧고 난해한 논문 세 편을 학술지에 내지도 않고 인터넷에 올린 뒤 떠났고, 세계 여러 연구팀이 4년에 걸쳐 논증을 해독하고 빈틈을 메운 끝에야 옳다고 선언했다. 앤드루 와일스의 페르마의 마지막 정리는 1993년 발표 뒤 심사 과정에서 결함이 드러나, 와일스와 리처드 테일러가 2년을 더 매달린 끝에 겨우 메웠다. 한 사람이 쓰는 시간과 세계가 확인하는 시간의 격차는 이미 이렇게 컸다.

여기에 AI가 더해진다. 2년 전만 해도 입문 수준 경시 문제에서 쉽게 무너지던 모델이 이제 국제수학올림피아드에서 최상위권과 겨루는데, AI가 네 시간 만에 내놓은 풀이를 사람 전문가는 한 시간씩 붙잡고 확인해야 한다. 강연자는 곧 하루에 한 편이 아니라 수천 편의 증명이 리만 가설이나 나비에-스토크스, P 대 NP 같은 문제를 향해 쏟아질 것이라고 본다. 게다가 이 모델들은 인터넷의 사람 글로 학습하고 사람 피드백으로 다듬어지므로, 사람의 편향과 허술한 추론이 미래의 발견 엔진에 그대로 구워진다.

해법으로 제시된 것이 형식 수학이고, 그 설계도는 400년 전 라이프니츠가 그렸다. 그가 꿈꾼 보편 기호학은 완벽한 논리 언어와 검증된 지식의 대백과사전, 그리고 거기서 새 사실을 기계적으로 끌어내는 '이성의 엔진' 세 부분으로 이뤄지는데, 강연자는 2025년에 이르러 처음으로 세 부품이 다 갖춰졌다고 말한다. 논리 언어는 증명 보조기 Lean, 백과사전은 약 200만 줄 규모의 오픈소스 Mathlib이고 남은 엔진 자리를 AI가 채운다. AI가 Lean으로 증명을 써 내놓으면 사람은 한 줄씩 따라갈 필요 없이 컴파일러에 넣어 빌드가 통과하는지만 보면 되므로, 맹목적 신뢰 대신 기계 검증에 기대며 사람은 질문을 던지고 방향을 정하는 자리로 옮겨간다.

주요 인사이트

• 생성은 급격히 싸지는데 검증은 그대로 비싸다는 비대칭이 이 강연의 출발점이다. AI 시대의 병목은 아이디어가 아니라 확인 절차 쪽에 생긴다.
• 형식화는 성능을 높이는 기술이 아니라 신뢰 구조를 바꾸는 장치다. '이 모델을 믿을 수 있는가'라는 질문이 '이 증명이 컴파일되는가'라는 기계적 질문으로 대체된다.
• 학습 데이터와 피드백이 사람에게서 오는 한 사람의 오류도 함께 학습된다. 형식 검증은 이 고리를 끊는 지점에 놓인다.
• 라이프니츠의 구상이 수백 년 동안 실현되지 못한 이유는 발상이 아니라 부품이었다. 형식 증명이 요구하는 기계적 정밀함은 사람의 창의성과 잘 맞지 않아, 엔진 자리를 채울 존재가 없었다.
• 사람의 역할은 사라지는 것이 아니라 이동한다. 강연자는 사람이 검토자 자리에서 내려와 탐험가이자 설계자, 질문하는 사람 자리로 옮겨간다고 표현한다.

자주 묻는 질문

관련 AI 소식