AI가 쓴 수학 원고 722편이 한꺼번에 나온 뒤 2주 동안 많이 읽힌 글 여럿이 같은 문제를 짚었어요. 확인하고 이해하는 속도가 만들어 내는 속도를 따라가지 못한다는 거예요. OpenAI가 10월 6일 공개 저장소 openai/math에 올린 원고 가운데 세 편은 이튿날 철회됐어요. 필즈상 수상자 한 사람은 울었다고 털어놓았지만 ‘지금만큼 수학 하기 좋은 때는 없었다’는 제목의 영상도 화제가 됐어요. 이 일을 다룬 글 가운데 10월 19일까지 Hacker News(HN) 상위에 오른 것을 모아 읽었어요.
원고 722편, 문제 4,000개
OpenAI는 원고와 Lean 증명을 GitHub의 공개 저장소 openai/math에 올렸어요. 처음 올린 README에는 원고가 722편이고 서로 이어진 원고끼리 372개 묶음으로 나눴다고 적혀 있어요. 대부분은 공개하지 않은 사내 모델로 같은 절차를 밟아 얻은 결과예요. 결과 하나에 ChatGPT Pro 수준의 추론을 평균 3시간 들였고 모델에 맡긴 문제는 4,000개쯤이에요.
Scott Aaronson은 블로그에서 이렇게 계산했어요. 여러 해 풀리지 않던 문제를 이 모델에 맡기면 3시간짜리 시도 한 번으로 열에 하나쯤은 푼다는 거예요. 공개된 결과에는 Subhash Khot의 유니크 게임 추측(Unique Games Conjecture) 증명도 들어 있어요. 다만 README를 보면 결과마다 검증 단계가 달라요. 모든 결과를 Lean으로 형식화한 것은 아니라서 ‘형식화하지 않은 결과에는 문제가 있을 수 있다’는 문장도 함께 적혀 있어요.
OpenAI가 처음 공개한 원고는 722편이에요. 점 하나가 원고 하나예요.
서로 이어진 원고끼리 372개 묶음으로 나뉘어 있어요. 점의 자리는 원고 순서와 관계없어요.
이튿날인 10월 7일, 이 가운데 세 편이 철회됐어요. 남은 원고는 719편이에요.
한 원고의 부호 오류 하나가 같은 구성을 쓰던 원고 두 편까지 무너뜨렸어요.
같은 날 기준으로 남은 719편 가운데 대표 결과 300개, 약 42%가 Lean으로 형식화됐어요.
나머지는 아직 컴퓨터가 증명을 한 단계씩 확인하지 않은 원고예요.
이튿날 철회된 세 편
10월 7일, 저장소의 변경 기록(history.md)에 호지 추측과 관련된 원고 세 편을 철회한다는 내용이 올라왔어요. 이유는 짧아요. 한 원고에 부호 오류가 하나 있어 상쇄 논증이 성립하지 않았고 같은 구성을 가져다 쓴 원고 두 편도 함께 내렸다는 거예요. 철회 공지에는 ‘증명을 철회하는 것이지 명제가 거짓이라는 뜻은 아니다’라는 문장도 붙어 있어요. 같은 날 OpenAI는 다른 원고 14편의 증명을 보완하거나 명제를 바로잡았고 Lean 형식화 6편을 새로 보탰어요. 그 결과 남은 원고 719편 가운데 대표 결과 300개, 약 42%가 형식화됐어요.
OpenAI의 Dan Roberts가 이 소식을 X에 올리자 좋아요 1,804개가 달리고 조회수는 54만 회를 넘었어요. HN에서는 381점에 댓글이 612개 달렸어요. README에는 ‘일부 결과는 모델이 앞서 낸 결과를 바탕으로 했다’는 문장도 있어요. 오류 하나가 원고 세 편으로 번진 것도 그래서예요.
Lean이 확인하는 것과 확인하지 않는 것
증명 보조기 Lean으로 형식화한 결과는 컴퓨터가 증명을 한 단계씩 검사해요. Thomas Hales는 Terence Tao의 블로그에 실은 객원 글에서 이 보장이 어디까지인지 짚었어요. 커널이 통과시킨 증명이라도 커널에 버그가 있으면 틀릴 수 있어요. 올여름에는 Lean의 버그 하나 때문에 콜라츠 추측을 ‘반증’하는 잘못된 증명이 나오기도 했어요(지금은 고쳐졌어요). 더 흔한 함정은 명제 쪽에 있어요. Lean은 증명이 명제와 맞는지 확인할 뿐 그 명제와 정의가 우리가 뜻한 내용인지는 확인하지 않아요.
Lean으로 쓴 증명이라도 명제가 뜻한 그대로인지 사람이 직접 검토하기 전에는 받아들이지 말아야 한다.
Thomas Hales, Terence Tao의 블로그 객원 글
Hales는 이 검토가 증명 자체를 확인하는 일보다 대개 훨씬 쉽다고 덧붙였어요. 제가 보기에 42%라는 숫자는 출발점이에요. 형식화하지 않은 원고에는 형식화가, 형식화한 원고에는 명제 검토가 남아 있어요.
누구는 울고 누구는 반기고
Derek Thompson은 칼럼 「I know why the mathematicians weep」(수학자들이 왜 우는지 안다)에서 수학계의 반응을 모았어요. HN에서 397점을 받은 글이에요. 2022년 필즈상을 받은 Hugo Duminil-Copin은 10월 공개 뒤 이렇게 말했어요.
화요일 밤에 울었는데 그 소리에 딸이 깼다. 그 사람들이 내 연구 분야를 없애 버렸다.
Hugo Duminil-Copin, Derek Thompson의 글에서
Terence Tao는 공개 당일 Mathstodon에 네 편짜리 글타래를 올렸어요(HN 614점). Tao가 ‘Math 1.0’이라고 부르는 예전 방식에서는 오래된 추측이 풀리면 증명한 사람이 여기저기 강연을 다니고 워크숍이 열려요. 공동 연구와 후속 문제가 생기고 새로운 사람들이 그 분야로 들어와요. 그러는 사이 증명은 다듬어져 다음 세대의 교과서에 실려요. Tao는 지금은 그 반대가 흔하다고 썼어요. AI로 문제를 푼 사람이 결과를 설명할 만큼 이해하지 못한 채 다음 문제로 넘어가고 뒤따르는 세미나와 공동 연구도 훨씬 적다는 거예요. 유망한 연구 방향을 남에게 뺏길까 봐 공개하지 않는 일까지 생겼다고 해요.
미해결 문제의 답을 지금처럼 대량으로 거둬들이는 방식은 오래 갈 수 없다.
Terence Tao, Mathstodon, 2026-10-06
Tao가 말하는 ‘Math 2.0’은 문제 풀이뿐 아니라 해설을 쓰는 일, 공동체를 꾸리는 일, 새 연구 방향을 여는 일까지 수학의 진전으로 인정하자는 제안이에요. Tao는 AI가 이 모든 일에 보탬이 될 수 있다고 봐요. 다만 마음에 드는 AI 에이전트에 미해결 문제를 던져 놓고 답을 받아 오는 것보다 더 큰 상상력과 야심이 필요하다고 했어요.
Aaronson의 글(HN 409점)은 결이 조금 달라요. 공개된 결과 가운데 일부는 Lean으로 검증됐지만 이 증명을 제대로 이해한 사람은 아직 거의 없다고 했어요. 그러면서도 ‘AI로 우리 미해결 문제를 풀어 재미를 망치지 말라’는 주장은 전혀 받아들일 수 없다고 못 박았어요. 이런 능력은 어차피 GPT나 Claude를 구독하는 사람이면 누구나 쓰게 된다는 거예요.
이번에 나온 증명을 제대로 이해한 사람은 아직 거의 없다. 이해하려는 경주는 이제 막 시작됐다.
Scott Aaronson, The Mathocalypse
Aaronson은 AI가 낸 수학 성과를 세상에 알리는 방식이 두 갈래로 굳어지고 있다고 봐요. 하나는 OpenAI처럼 AI가 쓴 증명을 손대지 않고 그대로 공개하는 방식이에요. 다른 하나는 Anthropic의 방식이에요. Virginia Williams와 Josh Alman은 Anthropic 모델이 내놓은 핵심 아이디어로 3SUM 문제와 모든 쌍 최단 경로 문제의 알고리즘을 개선했어요. Anthropic은 날것의 결과를 바로 내놓지 않고 두 사람에게 보수를 주어 내용을 소화해 다시 쓴 논문으로 발표하게 했어요. Aaronson은 두 방식 모두 장단점이 있다고 했어요. OpenAI 방식에서는 난삽한 증명을 누가 먼저 풀어내나 하는 경쟁이 벌어져요. Anthropic 방식에서는 AI의 성과를 전할 수학자를 회사가 고르게 되고요.
같은 시기에 3Blue1Brown의 영상 「There’s never been a better time to go into math」(지금만큼 수학 하기 좋은 때는 없었다)도 HN에서 541점을 받았어요. 제목만 봐도 분위기가 정반대예요. 영상 내용은 이 글에서 다루지 않았어요.
코드에도 똑같이 남는 질문
제가 보기에 이 이야기는 AI가 코드를 쓰는 요즘 개발 현장과 꼭 닮았어요. Lean 커널의 검사는 테스트와 타입 검사에 해당해요. 명제가 뜻한 그대로인지 보는 검토는 사람이 명세를 읽는 코드 리뷰고요. Tao가 말한 후속 활동은 그 코드를 이해하는 사람이 팀에 남아 있는 일이에요.
기계가 돌리는 검사부터 갖춰요. 테스트, 타입, 형식 검증처럼 사람 없이도 도는 검사예요.
그 검사가 무엇을 확인하는지는 사람이 봐요. 테스트가 엉뚱한 명세를 지키고 있으면 초록불은 아무 의미가 없어요.
설명할 수 있는 사람을 남겨요. 결과를 설명할 사람이 없으면 다음 사람이 그 위에 더 쌓을 수 없어요.
원고 722편이 한꺼번에 쏟아지자 수학계에서는 확인하고 이해하는 속도가 만들어 내는 속도를 따라가지 못하게 됐어요. 수학에서도 코드에서도 이제 그 틈을 메워야 해요.