증명이 넘쳐나는 시대의 수학 — Terence Tao의 「Math 2.0」이 다시 묻는 가치

AI가 증명을 대량으로 생산할 수 있게 되었을 때, 수학이 지켜야 할 것은 「먼저 푼 사람」의 영예인가, 「이해한 사람」의 공동체인가?

도입

2026년 10월 11일 해커뉴스 1면에 Terence Tao의 강연 슬라이드 「Math 2.0」 PDF가 올라와 563점을 받았다. 파일 이름에는 Caltech와 2026이 들어 있고, 표지에는 「October 2026」이라고만 적혀 있다.

이 슬라이드는 진공 속에서 나온 것이 아니다. 같은 주에 세 가지 일이 연달아 있었다. 10월 6일(미국 시간) OpenAI는 내부 미공개 모델이 만든 수학 원고 묶음을 GitHub 저장소 openai/math로 공개했고, 해커뉴스에서 「Sharing AI progress in mathematics」라는 제목으로 1,362점을 받았다(해커뉴스 기준 10월 7일). 같은 날 Tao는 Mastodon에 네 개짜리 스레드를 올려 「Math 2.0은 수학적 진보를 더 총체적으로 평가해야 한다」고 썼고, 이 글은 10월 8일 해커뉴스에서 614점을 받았다. 그리고 10월 8일에는 Dan Roberts(X 계정 danintheory)가 「우리의 GitHub math 저장소」를 갱신했다며 세 편의 철회를 공지했고, 이 소식도 381점을 받았다.

이 블로그는 9월 5일 페르마의 마지막 정리 형식화를 다루며 「검증되었지만 읽히지 않는 증명」이 지식인가를 물었다. 그때의 질문은 한 편의 거대한 증명에 관한 것이었다. 이번 주에 벌어진 일은 규모가 다르다. 수백 편이 한꺼번에 쏟아졌고, 그중 일부는 형식 검증을 거쳤고 일부는 거치지 않았으며, 그중 일부는 사흘 만에 철회되었다. Tao의 슬라이드는 이 상황을 개별 증명의 진위가 아니라 수학이라는 분야의 「보상 구조」 문제로 다시 짠다. 이 글은 그 재구성이 무엇을 주장하는지, 그리고 어디가 약한지를 따져 본다.

현상 분석 — 일주일 동안 쏟아진 증명들

먼저 사실관계부터 정리하자. 출처는 OpenAI 저장소의 README와 history.md이며, 이 글을 쓰는 시점(10월 18일)에 확인한 내용이다. OpenAI의 공식 발표 페이지는 접근이 차단되어 직접 확인하지 못했다.

README에 따르면 저장소는 「내부 OpenAI 모델이 생산한 수학 원고와 그 증명 산출물」을 담고 있으며, 현재 719편의 원고가 372개의 「패밀리」로 묶여 있다. 생산 방식도 적혀 있다. 대부분의 결과는 미공개 내부 모델로 같은 절차를 따라 얻었고, 결과 하나당 평균 ChatGPT Pro 사고(thinking) 연산 약 3시간이 들었다. 평가 기간 동안 모델에게 약 4,000개의 문제가 주어졌고, 이를 패밀리와 원고로 묶고 「적절한 수준의 중요성」을 요구해 걸러 낸 것이 지금의 목록이다. 예외도 명시되어 있다. 리만 제타 함수의 영점 없는 영역에 관한 작업과 CM 아벨 다양체에 대한 호지 추측의 증명은 이 고정 절차의 예외이며, Re(s) > 11/12 영역에 대한 원고는 가독성을 위해 사람이 편집했다고 한다.

검증 상태에 대해서는 README 스스로 조심스럽다. 「모든 결과에 Lean 형식화가 딸려 있지는 않다」, 「형식화되지 않은 결과 중 일부는 문제가 있을 수 있다」고 적는다. history.md의 10월 7일 항목은 이를 구체적으로 보여 준다. 「분할 아벨 8차원 다양체 위의 Weil 류의 대수성」 원고에서 부호 오류가 발견되어 안정화-트레이스 상쇄 논증이 무너졌고, 그 구성을 쓰는 두 편의 의존 원고와 함께 세 편이 철회되었다. 같은 항목에서 14편이 증명 보수와 가설 명확화로 수정되었고, 13편이 수정된 동반 원고를 인용하도록 갱신되었다. 형식화는 6건이 추가되어 「최상위 결과의 형식화 비율」이 300/719, 약 42%가 되었다고 한다. 철회된 세 편이 Lean으로 형식화된 결과였는지는 이 문서만으로는 확인되지 않는다. 해커뉴스에서도 바로 그 질문이 반복되었다.

OpenAI의 공개 직전에는 또 하나의 맥락이 있다. AGMAI라는 수학자 자문 그룹은 9월 29일 「AI 생성 수학의 책임 있는 공개」라는 권고를 냈다. 이들은 600건 이상의 응답을 모아 권고를 만들었다고 밝히며, 수학 공동체의 가장 중요한 규범 중 하나는 「저자가 논문의 수학적 논증을 이해하고, 스스로 정확성을 검증하고, 내용에 전적인 책임을 지는 것」이라고 적었다. 그리고 AI 연구소가 즉각적인 인간의 이해 없이 대량의 수학적 결과를 공개한다면 「인간의 이해가 뒤따르도록 책임져야 하며」, 그 이해의 발전은 「공동체 주도로 유기적이어야 한다」고 권고했다. 서두에서는 아예 연구소들이 비공개 독점 모델로 고급 수학 문제를 시험하는 관행 자체를 지지하지 않는다고 못 박았다.

해커뉴스의 반응은 크게 갈렸다. OpenAI 공개 스레드에서 한 이용자는 이 목록이 자신이 참고하는 「상위 500개 미해결 문제」 중 90개를 완전히 풀었다고 주장한다고 집계했다(직접 인용은 아니고, 코멘트의 요지를 요약)(@zone411). 다른 이용자는 박사 과정 중간에 비슷한 결과의 원고를 절반쯤 써 둔 학생이라면 이제 무엇을 해야 하느냐고 물었다(직접 인용은 아니고, 코멘트의 요지를 요약)(@open592). 또 다른 이용자는 Lean이 증명 인증서로 기능하려면 정리의 진술 자체가 올바르게 표현되어야 하는데, 이렇게 넓은 분야에 걸쳐 그것을 보장하기는 어렵다고 경고했다(직접 인용은 아니고, 코멘트의 요지를 요약)(@mathisfun123). 철회 스레드에서는 이 경고가 현실이 된 듯한 반응이 이어졌다. 「Lean으로 검증된 것 아니었나」라는 질문, 그리고 400편 가까운 결과 중 세 건의 실수면 꽤 좋은 적중률이라는 반론(@hmate9), 검증의 부담은 리뷰어에게 넘어가고 공은 제안자가 가져간다는 지적(@BenoitP)이 나란히 놓였다(모두 직접 인용은 아니고, 코멘트의 요지를 요약).

심층 분석 — 「증명의 희소성」이라는 숨은 전제

Tao의 슬라이드가 흥미로운 이유는, 이 소란을 「AI 증명은 믿을 만한가」라는 질문으로 다루지 않는다는 데 있다. 그는 오히려 반대쪽에서 출발한다. 증명은 다른 분야에서는 드문 성질, 곧 「객관적으로 검증 가능하다」는 성질을 갖는다. 어떤 수학이 흥미로운지에 대해서는 수학자들 사이에 이견이 있어도, 무엇이 올바르고 완전한 증명인지에 대해서는 넓은 합의가 있으며, Lean 같은 증명 보조기로 쓰면 컴퓨터가 기계적으로 검사할 수도 있다. 게다가 증명은 고도로 디지털화 가능하다. 물리적 실험도, 현실 세계의 데이터도 필요 없고, 관련 문헌의 상당 부분이 이미 디지털로 존재한다.

Tao의 논리는 여기서 뒤집힌다. 객관적 검증 가능성, 디지털화 가능성, 대규모 고품질 데이터라는 세 성질이 겹친 덕분에 수학 문제 풀이는 기계 학습에 특히 잘 맞는 과제가 되었고, 프런티어 AI 연구소들은 이 세 성질 중 하나라도 결여된 다른 응용보다 수학을 우선시했다. 그 결과 우리는 「증명 풍요(proof abundance)」의 시대에 들어서고 있다는 것이다. 수학의 미덕이 곧 수학의 취약점이 된 셈이다.

여기서 핵심 개념이 「증명 희소성(proof scarcity)」이다. Tao는 전통 수학, 곧 「Math 1.0」의 제도와 전통, 인센티브, 공식 목표의 상당수가 「미해결 문제의 해답을 찾고 증명하는 것은 어렵고 드물며 상당한 인간 전문성을 요구한다」는 가정 위에 조직되었다고 본다. 그리고 문제 풀이는 역사적으로 연구 수학의 가장 눈에 띄는 목표였지만 사실은 더 가치 있는 장기 목표의 「대리 지표(proxy)」였다고 말한다. 희소성의 시대에는 이 대리 지표가 대체로 정확했다. 그러나 풍요의 시대에는 어긋났고, 문제 풀이만을 맹목적으로 최적화하는 것은 이제 수학의 장기적 건강에 「적극적으로 해롭다」는 것이 그의 결론이다.

이 진단의 구체적 메커니즘은 슬라이드보다 Mastodon 스레드에 더 자세하다. Math 1.0에서 오래된 추측의 돌파적 증명은 후속 활동을 대량으로 낳는다. 저자는 강연에 초대되고, 워크숍이 열리고, 새 협업이 생기고, 후속 문제가 공유되며, 젊은 수학자들이 그 분야로 끌려온다. 그 과정에서 증명은 소화되고 다듬어지고 맥락 속에 놓여 결국 다음 세대의 교과서가 된다. 그런데 지금은 그 반대가 자주 벌어진다고 Tao는 쓴다. 목표가 「해결」되고 나면 그 분야에 관심이 없는, 결과에 대해 질문에 답하거나 강연을 할 만큼 AI 출력을 이해하지 못하는 「AI 프롬프터」들이 문제를 자율적으로 풀어 버린다. 세미나도 협업도 덜 생기고, 그 분야에 합류하는 사람도 적으며, 유망한 미해결 방향은 「선수를 빼앗길까 봐」 공개되지 않고 있다.

그리고 이 과정은 되돌릴 수 없다. 한 번 「풀린」 문제를 다시 「안 풀린」 상태로 되돌릴 수는 없고, 해답이 존재한다는 사실만으로도 다른 경로를 찾으려는 노력이 「오염」된다. Tao는 그래서 미해결 문제의 해답이 지속 불가능한 방식으로 대규모 「수확」되고 있으며, 분야 전체가 덜 비옥해지고 있다고 표현한다. 슬라이드의 「등대」 비유가 이 지점을 받친다. 순수수학의 미해결 문제는 그 자체로 도달해야 할 목적지가 아니라 주변 지형을 탐험하게 하는 안내자이고, 성공하든 실패하든 부분적 진전에 그치든 그 과정에서 얻는 교훈이 최종 해답보다 더 가치 있는 경우가 많다. 자동화된 도구로 등대에 너무 일찍 도착하면 가지 않은 길의 탐험이 끊기고 주변 분야가 「불모화」될 수 있다는 것이다.

이 논리는 소프트웨어 엔지니어에게도 낯설지 않다. 벤치마크가 학습 목표가 되는 순간 벤치마크는 측정 도구로서의 의미를 잃는다는 굿하트의 법칙과 같은 구조다. 해커뉴스 Tao 스레드에서 한 이용자는 소프트웨어 개발은 결과물이 목적이라 수단이 바뀌어도 산업이 무너지지 않지만, 수학 연구에서는 과정이 곧 결과물이라는 대비를 소개했다(직접 인용은 아니고, 코멘트의 요지를 요약)(@theturtletalks).

전망과 시사점 — 무엇을 평가할 것인가

그렇다면 Tao는 무엇을 대신 평가하자고 하는가. Mastodon 스레드의 마지막 글에서 그는 Math 1.0이 「초기에는 잘 이해되지 않더라도 미해결 문제를 처음 푼 사람」에게 프리미엄을 주었다고 쓰고, Math 2.0은 문제 풀이의 역할을 탈중심화하고 해설(exposition), 공동체 구축, 새로운 연구 방향의 개척을 높이 평가해야 한다고 말한다. 그리고 수학 공동체는 교육, 출판, 경력 승진의 기준을 명시적으로 재평가해야 한다고 덧붙인다. 「먼저 푼 사람」의 영예라는 오래된 신용 체계를 정면으로 겨눈 말이다.

슬라이드는 이를 구체적 사례로 채운다. 증명이 불투명한 기존 결과에 동기가 분명한 설명을 찾는 「미해결 해설 문제(open exposition problems)」, 많은 논문을 하나의 살아 있는 네트워크로 엮는 시도(명시적 해석적 정수론 네트워크 IEANTN), Mathlib 같은 대규모 고품질 형식 수학 라이브러리, 이미 증명된 정리에서 핵심 입력을 제거해도 여전히 증명되는지 보는 「절제 연구(ablation study)」, 가설을 바꾸거나 버렸을 때 무엇을 건질 수 있는지 탐색하는 「정리의 이웃」 탐사가 그것이다. 대규모 데이터셋에 기반한 실험 수학도 제시된다. 2,200만 개 이상의 참/거짓 명제를 정리한 Equational Theories Project, 차수 24에서 가능한 25,000개의 갈루아 군 각각에 대응하는 다항식을 찾는 역 갈루아 문제 챌린지가 예다. 「사례 연구」가 아니라 「모집단 조사」라는 표현이 인상적이다.

여기서 Lean의 위치가 달라진다는 점에 주목할 만하다. Math 1.0의 논리에서 형식 검증은 「이 증명이 맞는가」를 판정하는 도구였다. Tao의 Math 2.0 목록에서 형식화는 Mathlib처럼 공동체가 공유하고 쌓아 올리는 「라이브러리」로 등장한다. 그리고 그의 사고 실험은 Lean 인증서가 있어도 충분하지 않은 경우를 겨눈다. AI가 암 치료용 화합물 칵테일을 찾아내 Lean 인증서까지 붙이고 3상 임상시험을 통과했지만 아무도 그 발견 경위를 모른다면, 그 해답이 시험 절차나 수학적 모델의 약점을 파고든 「정렬되지 않은(misaligned)」 해답일 가능성은 없는가. Tao는 이를 「강력한 AI + 인간 이해의 결여 = 정렬 위험」이라고 요약한다. 이는 철회 사건과 정확히 맞물린다. 형식 검증은 진술이 올바르게 옮겨졌다는 전제 위에서만 의미가 있고, 그 전제를 확인하는 것은 결국 이해하는 사람이다.

다만 이 사고 실험은 해커뉴스에서 가장 많은 반발을 받은 부분이기도 했다. 말기 환자라면 아무도 이해하지 못하는 치료라도 받겠다는 반응(@qup), 전신 마취처럼 작용 기전이 완전히 밝혀지지 않은 약이 이미 널리 쓰인다는 지적(@squidmaster)이 상위에 올랐다(모두 직접 인용은 아니고, 코멘트의 요지를 요약). 이 반론은 일리가 있지만 Tao의 요점을 약간 비껴간다. 그의 사분면은 「인간 이해가 약한 상태」 자체를 위험이라 부르지 않는다. 그것은 단지 아직 충분히 수학화되지 않은 상태일 뿐이며, 위험은 그 결여가 AI의 최적화 능력과 결합할 때 생긴다는 것이다.

더 날카로운 반론은 「설명도 결국 AI가 더 잘하게 되지 않겠느냐」는 것이다. Tao의 Mastodon 글을 다룬 해커뉴스 스레드에서 한 이용자는 모델 지능이 계속 오르면 수학자가 모델에게 증명을 단계별로 설명해 달라고 하면 그만이니 이해의 간극은 사라질 것이라고 주장했다(직접 인용은 아니고, 코멘트의 요지를 요약)(@vasco). Tao 슬라이드도 이 가능성을 배제하지 않는다. 그가 제시하는 목록 자체가 AI를 해설과 네트워크 구축에 쓰자는 것이기 때문이다. 다만 해설이 AI로 해결되더라도, 「누가 이해했는가」, 「누가 책임지는가」라는 AGMAI의 질문은 남는다. 또 다른 이용자는 AI가 저렴하지 않아 부유한 나라의 좋은 대학이 유리해질 것이라고 지적했다(직접 인용은 아니고, 코멘트의 요지를 요약)(@contubernio). 평가 기준을 바꾸는 일은 자원 배분을 바꾸는 일과 분리될 수 없다.

결론

Tao의 「Math 2.0」은 AI 증명이 맞는지 틀렸는지를 다투는 글이 아니다. 오히려 AI 증명이 대체로 맞을 수 있다는 전제에서 출발해, 그렇다면 수학이라는 분야가 무엇을 보상해 왔는지를 다시 묻는다. 그의 답은 「문제 풀이는 대리 지표였다」는 것이다. 희소성의 시대에는 풀이가 이해와 공동체와 후속 연구를 함께 끌고 왔기에 둘을 구별할 필요가 없었다. 풍요의 시대에는 풀이만 따로 떨어져 나온다.

같은 주의 철회 사건은 그 분리가 어떤 비용을 낳는지 보여 준다. 719편의 원고 중 약 42%만 형식화되어 있고, 나머지를 확인할 책임은 사실상 공동체에 넘어간다. 그 공동체가 줄어들고 있다는 것이 Tao의 경고다. 그가 마지막 슬라이드에 적은 말은 의외로 낙관적이다. Math 2.0의 주된 병목은 기술도, 제도 문화도 아니고 「상상력」이라는 것이다.

당신의 분야에서 「먼저 해낸 사람」에게 주던 신용은 무엇의 대리 지표였는가. 그 대리 지표가 기계에게 넘어갔을 때, 원래 지키려던 것을 무엇으로 셀 것인가.

출처: