필즈상 수학자의 선언
지금 살아 있는 수학자 중 가장 유명한 사람 하나를 꼽으라면 테렌스 타오(Terence Tao)를 빼기 어려운데요. 그가 블로그에 ‘Mathematics has changed. Let's act like it’이라는 제목의 글을 올렸어요. 우리말로 옮기면 “수학은 이미 바뀌었다. 이제 그에 맞게 행동하자” 정도예요. 타오는 2006년에 필즈상을 받은 UCLA 교수예요. 최근 몇 년 동안은 AI와 형식 증명 도구를 수학 연구에 가장 적극적으로 끌어들여 온 사람이기도 하고요.
제목에서 눈여겨볼 단어는 ‘이미’예요. 언젠가 바뀔 거라는 예측이 아니에요. 변화는 벌써 일어났고, 이제 수학계의 습관과 제도가 그걸 따라잡아야 한다는 메시지죠. 타오가 말하는 변화가 뭔지 감을 잡으려면, 그가 최근에 직접 해 온 실험들을 보면 돼요.
타오가 직접 보여준 세 가지 변화
1. 증명을 컴파일러가 검사한다
Lean은 ‘증명 보조기(proof assistant)’라고 부르는 도구예요. 이게 뭐냐면, 수학 증명을 프로그래밍 언어처럼 작성하면 컴퓨터가 한 줄 한 줄 논리적으로 맞는지 검사해 주는 거예요. 코드가 컴파일되면 문법과 타입이 맞다는 게 보장되잖아요. 마찬가지로 Lean에서 증명이 통과하면 논리에 빈틈이 없다는 게 보장돼요. 물론 증명하려는 명제를 Lean에 제대로 옮겨 적었다는 전제에서요. 2023년에 타오는 고워스, 그린, 매너스와 함께 다항식 프라이만-루자(PFR) 추측을 증명했어요. 그리고 이 증명을 Lean으로 옮기는 온라인 협업 프로젝트를 직접 이끌었는데, 약 3주 만에 끝났어요.
2. 수십 명이 함께 푸는 수학
2024년에는 ‘방정식 이론 프로젝트(Equational Theories Project)’를 진행했어요. 마그마라는 아주 단순한 대수 구조가 대상이었어요. 연산이 하나뿐인 집합이라고 생각하면 돼요. 마그마에 대한 등식 법칙 4천여 개 사이에서, 어떤 법칙이 다른 법칙을 함축하는지 약 2,200만 쌍을 전부 판정하는 프로젝트였죠. 많은 참여자와 자동 정리 증명기가 함께 작업했고, 결과는 Lean으로 검증됐어요.
여기서 핵심은 신뢰의 문제예요. 원래 수학자는 모르는 사람의 증명을 쉽게 믿을 수 없어요. 하나하나 다 검토해야 하니까요. 그런데 Lean이 검증해 주면 누가 기여했든 결과를 믿을 수 있어요. 오픈소스 프로젝트도 똑같아요. CI가 테스트를 돌려주니까 처음 보는 사람의 PR도 안심하고 머지할 수 있잖아요.
3. AI가 연구 조수가 되다
타오는 구글 딥마인드의 AlphaEvolve를 여러 수학 문제에 적용해 보는 연구에도 참여했어요. AlphaEvolve는 LLM이 코드를 고쳐 가면서 더 나은 답을 찾아가는 탐색 시스템이에요. 오래된 미해결 문제 모음인 에르되시 문제들에서는 AI가 잊혀 있던 기존 논문을 찾아내거나 일부 문제 해결에 기여한 사례도 나왔어요. AI가 계산기를 넘어 연구 조수 역할을 하기 시작한 거죠.
그에 맞게 행동하자는 건 무슨 뜻일까
지금의 수학계 제도는 대부분 종이와 펜으로 혼자 증명하는 수학자를 전제로 만들어졌어요. 그러니 이런 질문들이 자연스럽게 따라와요. 수십 명과 AI가 함께 만든 결과라면 공로는 누구 몫일까요? Lean으로 검증된 증명이라면, 논문 심사는 정확성 대신 얼마나 중요한 결과인지에 집중해도 되지 않을까요? 대학원생에게 Lean과 AI 도구 쓰는 법을 가르쳐야 할까요? 변화를 인정한다는 건 결국 이런 질문에 답하기 시작하자는 뜻이에요.
업계는 어떻게 움직이고 있나
2024년 국제수학올림피아드(IMO)에서 딥마인드의 AlphaProof가 Lean으로 문제를 풀어 은메달 수준의 성적을 냈어요. 2025년에는 구글과 OpenAI의 모델이 자연어 풀이로 금메달 수준까지 올라왔고요. Harmonic 같은 스타트업은 아예 Lean 기반 수학 AI로 사업을 하고 있어요.
흐름을 보면 두 갈래가 합쳐지고 있어요. 자연어로 추론하는 AI는 빠르고 유연하지만, 그럴듯한 오답을 낼 수 있어요. Lean 같은 형식 검증은 느리지만 확실하죠. 그래서 AI가 증명을 만들고 Lean이 검증하는 조합이 주목받고 있어요. 어디서 많이 본 구조 같지 않나요? LLM이 코드를 쓰고 타입 체커와 테스트가 검증하는 요즘 개발 환경이랑 똑같아요.
한국 개발자에게 주는 시사점
사실 수학과 프로그래밍은 생각보다 가까워요. ‘커리-하워드 대응’이라는 개념이 있는데요, 쉽게 말하면 명제는 타입이고, 증명은 그 타입을 가진 프로그램이라는 거예요. 그래서 Lean은 증명 도구이면서 동시에 함수형 프로그래밍 언어이기도 해요.
AI 코딩이 일상이 된 지금은 개발자도 같은 질문을 받아요. AI가 만든 코드를 뭘 근거로 믿을 거냐는 거죠. 강한 타입 시스템, 속성 기반 테스트, TLA+나 Dafny 같은 형식 검증 도구가 다시 주목받는 이유예요. 속성 기반 테스트는 무작위 입력을 수백 개 넣어 보면서 규칙이 항상 지켜지는지 확인하는 테스트예요. AWS가 분산 시스템 설계를 TLA+로 검증해 온 건 이미 유명한 사례고요.
Lean이 궁금하다면 Natural Number Game으로 시작해 보세요. 브라우저에서 바로 할 수 있는데, 게임처럼 자연수의 성질을 하나씩 증명해 나가요. 생각보다 중독성이 있어요.
마무리
AI가 만들고 기계가 검증하는 시대가 됐어요. 바뀐 건 도구만이 아니라, 무엇을 믿을 수 있는지에 대한 기준이에요.
여러분의 팀은 AI가 작성한 코드를 뭘 근거로 믿고 있나요? 언젠가 소프트웨어도 ‘테스트를 통과했다’를 넘어 ‘증명됐다’가 기본이 되는 날이 올까요?
🔗 출처: Hacker News