2026년 10월, 캘리포니아 공과대학교(칼텍) 연단에 선 수학자 테렌스 타오는 직관을 뒤흔드는 경고를 던졌다. 현대 AI가 수학 연구를 전례 없는 역설 속으로 밀어 넣고 있다는 것이다. 지난 한 세기 동안 이어져 온 ‘증명의 희소성’은 이제 급격히 ‘증명의 과잉’ 시대로 바뀌고 있다.
지난 100년간 수학의 토대는 단 하나의 전제 위에 서 있었다. 바로 엄밀한 증명을 얻기가 대단히 어렵다는 사실이다. AI는 이 근본적인 전제를 무너뜨리고 있다. 본래 문제 해결은 학문적 진보를 가늠하는 척도였으나, 이제 문제 풀이 자체만을 궁극적인 목표로 삼는 태도는 오히려 수학이라는 학문을 안쪽에서부터 공동화할 위험이 있다.
연산력으로 1년에 2200만 개 명제 판정, 해답은 더 이상 희소하지 않다
전통 수학은 ‘증명의 희소성’을 바탕으로 구축되었다. 지난 세기 동안 미해결 추론 하나를 해결하려면 최고의 전문가들이 수년에 걸친 피땀 어린 노력을 쏟아야 했다. 학계 전체의 교수 임용 심사, 학술지 출판, 명성 체계 역시 이러한 희소성을 중심으로 돌아갔다.
이러한 수급 균형이 막대한 연산력에 의해 새로 쓰이고 있다. 타오는 강연에서 구체적인 실증 데이터를 제시했다. Equational Theories Project는 2024년부터 2025년 사이 인간과 기계의 협업을 통해 보편대수학에서 2200만 개가 넘는 명제의 참과 거짓을 판정했다.
그림: Equational Theories Project는 크라우드소싱 방식으로 2200만 개 이상의 명제를 판정했다. 출처: 테렌스 타오의 ‘Math 2.0’ 강연 슬라이드
이와 유사한 고속 진전이 여러 분야에서 동시다발적으로 벌어지고 있다. 2026년 역갈루아 문제 챌린지에서 협업 연구팀은 짧은 시간 안에 24차 체의 2만 5천 개 갈루아 군 전체에 대해 다항식을 하나씩 계산해 냈으며, 이후 프로젝트는 목표를 31차로 확장했다.
이러한 처리량은 손으로 직접 유도하던 전통적인 연구 일정을 완전히 뒤엎었다. 막대한 연산력이 투입되면서 수학 연구는 개별 정리를 수작업으로 해부하던 방식에서 데이터 기반의 총조사 형태로 탈바꿈하고 있다.
객관적 검증과 실험 불필요, 대규모 모델의 이상적인 훈련장이 된 수학
왜 최첨단 AI 연구소들은 생물학이나 사회과학보다 순수 수학을 그토록 선호할까? 근본적인 원인은 순수 수학이 지닌 매우 드문 두 가지 공학적 특성에 있다.
첫 번째 특성은 객관적인 검증 가능성이다. 수학자들은 어떤 추론이 더 중요한지에 대해서는 논쟁할 수 있지만, 도출된 결론이 맞는지 틀리는지에 대해서는 확고한 합의를 이룬다. Lean과 같은 대화형 정리 증명 도구를 활용하면 컴퓨터는 코드 수준에서 기계적으로 유도 과정을 검증할 수 있다.
두 번째 특성은 고도의 디지털 자기완결성이다. 수학적 증명에는 물리적인 매개체도, 현실 세계의 노이즈 섞인 데이터 입력도, 출력을 시험할 실험실도 필요하지 않다. 종이와 펜, 정형화된 수학 라이브러리, 그리고 이미 디지털화된 방대한 문헌만 있으면 기계학습 모델은 이 닫힌 고리 안에서 무한히 반복 훈련할 수 있다.
이 조건들을 모두 갖춘 분야는 드물다. 이 때문에 프론티어 AI 연구소들은 실용적인 응용 분야보다 수학 문제 해결 능력을 우선순위에 두어 왔다. 대회 점수는 기계가 자동으로 판정할 수 있고 보도자료에서도 매력적인 수치로 드러나기 때문이다.
그러나 모델의 추론 능력은 매우 울퉁불퉁한 형태를 보인다. 충분한 연산력을 쏟아부으면 전문가의 도움 없이도 공개 대회 문제를 뚫어내는 반면, 복잡한 상호작용과 현실 세계의 생생한 경험을 요하는 실제 과제 앞에서는 여전히 쉽게 멈춰 선다.
소셜 미디어에 비치는 인상은 전혀 딴판이다. 사람들의 눈에 띄는 것은 오직 AI가 풀어낸 성공 사례뿐이다. 타오는 현재 수학 최전선에 놓인 대다수 문제가 아무리 많은 연산력을 태워도 여전히 풀리지 않은 채 남아 있다고 경고한다. 수학 문제의 공간은 무한하며 난이도의 상한선도 없다. First Proof와 같은 플랫폼이 설립된 이유도 바로 여기에 있으며, 연산 자원 소모량과 실패한 시도 결과까지 모두 투명하게 공개하도록 요구한다.
도착점만 좇다가 주변 생태계를 무너뜨린다
순수 수학의 세계에서 미해결 문제는 단순히 열쇠로 따기를 기다리는 문이 아니다. 타오는 인상 깊은 비유를 들었다. 미해결 난제란 미지의 바다에 우뚝 솟아 있는 등대와 같다.
등대의 진정한 가치는 주변 항로를 환히 비추는 데 있다. 그곳을 향해 항해하는 과정은 종종 최종적인 해답보다 훨씬 더 값진 결실을 안겨 준다. 성공하든, 실패하든, 절반만 나아가든, 그 여정에서 얻은 교훈은 모두 소중한 자산이 된다.
그림: Math 1.0과 Math 2.0 연구 프론티어의 진화. 출처: 테렌스 타오의 ‘Math 2.0’ 강연 슬라이드
자동화 도구를 써서 등대 꼭대기에 너무 일찍 도착해 버리면, 그 사이의 바닷길을 끝까지 항해하는 사람은 아무도 남지 않는다. 고군분투하는 과정에서 자연스럽게 싹텄어야 할 이론, 도구, 직관은 태어날 이유를 잃어버린다. 문제 해결과 진정한 이해가 완전히 분리되는 것이다.
임상을 통과한 암 치료법, 기전도 모른 채 혈관에 투여할 수 있는가
역사적으로 문제 해결은 이해의 깊이를 점검하기 위한 대리 지표에 불과했다. 증명이 희소했던 시절에는 거대한 난제를 풀어내는 과정에서 늘 방대한 이론 체계가 함께 탄생했다. 그러나 증명이 과잉된 시대에는 무차별 연산 탐색으로 인해 대리 지표와 본질적인 목적이 직접 단절된다.
타오는 강연에서 하나의 사고실험을 제안했다. 어느 정상급 연구소에서 AI 모델을 훈련했다고 가정해 보자. 목표는 매우 분명하다. 도중에 어떤 실수도 없이 3상 임상시험을 통과할 수 있는 항암제 처방을 내놓는 것이다.
막대한 연산력을 소모한 끝에 모델은 알려지지 않은 화학 물질 처방을 엄밀한 정형 증명 코드와 함께 제시했다. 실제 임상시험에서도 그 처방은 기준을 완벽하게 통과했다. 그러나 어떤 과학자도 그 분자 기전을 이해하지 못한다.
만약 스스로 초기 암 진단을 받았고 기계가 바로 그 처방을 추천했다면, 혈관에 약물을 주입하기 전에 단 한 사람이라도—비록 부분적일지라도—그것이 왜 효과가 있는지 이해하고 있기를 바라지 않겠는가?
순수 수학의 검증 논리는 결국 현실 세계로 파급된다. 연구자들이 블랙박스 해답 앞에서 생각하기를 포기하는 데 익숙해진다면, 응용과학의 안전 토대 역시 소리 없이 무너져 내릴 것이다.
테렌스 타오의 처방: 연산력을 문제 풀이에서 인간의 이해를 돕는 도구로
기계가 불러온 과잉의 위기 앞에서 타오가 제시한 해법은 ‘Math 2.0’으로의 전환이다. 핵심은 계산 도구의 무게중심을 일방적인 문제 풀이에서 인간의 이해력을 확장하는 방향으로 옮기는 것이다.
대표적인 시도가 이른바 ‘설명 열린 문제(Open Exposition Problems)‘라는 새로운 과제다. 증명 자체는 알려져 있지만 그 유도 과정이 난해하고 불투명한 결과들에 대해 직관적이고 납득할 만한 설명을 찾아내는 작업이다. 칼텍에서 새롭게 개편된 매스매치(Mathathon)는 이러한 방향성을 향한 첫 실험이다.
협업 연구 네트워크와 정형 코드베이스 구축 역시 속도를 내고 있다. 명시적 해석적 정수론 네트워크는 흩어져 있던 학술 논문들을 지식 그래프로 엮어내고 있으며, 정형화 수학 라이브러리인 Mathlib은 알고리즘 검증을 위한 표준 기저를 제공한다.
연구자들은 연산력을 활용해 ‘정리 절제 실험’에도 나서고 있다. 특정 정리의 핵심 전제를 의도적으로 제거하여 결론이 유지되는지 관찰하거나, 입력 조건을 완화하여 정리 주변의 파생 공간을 탐색하는 방식이다.
이러한 시도들은 연산력을 새로운 방법론을 추출하는 데 사용하여 인간이 지식 지도의 지형을 선명하게 파악할 수 있도록 돕는다.
타오가 보기에 Math 2.0을 추진하는 데 가장 큰 병목은 연산 자원도, 조직 문화도 아닌 바로 인간의 ‘상상력’이다.
참고 링크:
- 테렌스 타오 칼텍 강연 ‘Math 2.0’ 강의 자료 및 슬라이드
- First Proof 정형 수학 벤치마크 플랫폼 (1stproof.org)
- Equational Theories Project 크라우드소싱 공동 연구 아카이브
- 역갈루아 문제 챌린지 (IGP24) 협업 기록
