2026년 10월 6일, OpenAI는 공식 블로그에 「Sharing AI progress in mathematics」를 올렸어요. 그리고 아직 공개하지 않은 내부 모델이 쓴 수학 원고 722편을 자사 GitHub 저장소에 한꺼번에 올렸어요. 공개 다음 날 OpenAI는 3편을 철회했어요. 같은 날 변경 기록에는, 철회 뒤 남은 원고 719편 가운데 Lean이라는 증명 검사 프로그램으로 증명이 맞는지 확인된 것이 약 42%라고 적었어요. 나머지 원고는 수학자가 직접 읽어야 맞는지 알 수 있어요.
OpenAI는 AI 모델에 수학 연구 문제 약 4,000개를 풀게 해, 그 결과를 원고 722편으로 한꺼번에 공개했어요
저장소 README에 따르면, 결과의 대다수는 미공개 내부 모델로 같은 절차를 밟아 얻었어요. OpenAI는 평가 기간 동안 모델에 연구 문제 약 4,000개를 냈고, 결과를 372개 묶음으로 정리했어요. 372는 결과를 낸 문제의 수이고, 결과 하나에 원고가 여러 편 딸릴 수 있어서 원고 수는 722편이 됐어요. 목록을 추린 기준으로 README에 적힌 것은 “적절한 수준의 중요성”을 요구했다는 한 줄뿐이에요. 4,000개 가운데 몇 개에서 실패했는지, 372개를 구체적으로 어떻게 골랐는지는 적혀 있지 않아요. 결과 하나에 쓴 연산량은 평균적으로 ChatGPT Pro가 3시간 동안 생각하는 데 드는 연산과 비슷하다고 OpenAI는 밝혔어요.
OpenAI는 이 작업을 모델 평가의 일부라고 설명했어요. 기존 수학 시험 문제는 모델이 거의 다 풀게 되어서, 아직 답이 없는 연구 문제로 평가 범위를 넓혔다고 했어요. 원고와 함께 Lean 형식화 일부, 모델의 추론 요약 10건, 연산량 추정, 시도한 문제 수 통계도 공개했어요.
모든 결과가 이 절차를 따르지는 않았어요. 리만 제타 함수의 영점 없는 영역 작업과 CM 아벨 다양체의 호지 추측 증명은 이 절차 밖에서 나왔고, Re(s) > 11/12 영점 없는 영역 원고는 사람이 읽기 좋게 고쳤다고 README는 밝혔어요. 이 발표는 OpenAI가 아직 내놓지 않은 모델의 성과 발표이기도 해요. 블로그는 이 모델을 “responsibly release”(책임 있게 출시)하려 한다고 적었어요.
공개 다음 날 OpenAI는 증명에 계산 실수가 있던 원고 3편을 철회했고, 이와 별개로 다른 원고 14편의 증명을 고쳤어요
저장소의 변경 기록(history.md) 10월 7일 항목에는 철회 3편, 증명 수정 14편, 인용만 바꾼 13편, 형식화 6건 추가가 함께 적혀 있어요. Retraction Watch도 공개 다음 날 철회가 나왔다고 보도했어요. 다만 철회 공지 본문에는 철회일이 10월 6일로 적혀 있어서, 변경 기록의 날짜와 하루 어긋나요.
철회는 「Algebraicity of Weil classes on split abelian eightfolds」라는 원고에서 시작됐어요. 철회 공지에 따르면 이 증명은 한 계산 단계에서 부호를 +1로 매겼는데, 실제 부호는 −1이었어요. 부호 하나를 반대로 쓴 탓에 0이 나와야 할 값이 0이 아닌 값(−2m)이 됐고, 그래서 증명이 기대던 정리(Eliashberg–Murphy 소거 정리)를 쓸 수 없게 됐어요. 이 원고의 구성을 가져다 쓴 K3 곡면 관련 원고 2편도 함께 철회됐어요. 공지는 “이 철회는 증명에 관한 것이고, 명제가 거짓이라는 뜻은 아니다”라는 문장으로 끝나요. 증명이 틀린 것과 명제가 틀린 것을 나눠서 적었어요.
증명을 고친 14편은 이 부호 실수와 원인이 달라요. 변경 기록은 이 14편을 증명 보수, 진술 수정 같은 별도의 이유로 고쳤다고 적었어요.
| 변경 종류 | 편수 | 내용(history.md 10월 7일 항목) |
|---|---|---|
| 철회 | 3편 | 부호 실수가 있던 원고 1편과, 그 구성에 기대던 K3 곡면 관련 원고 2편 |
| 증명 수정 | 14편 | 립시츠 높이 4편, 켈러 MMP 6편, taming 2편, 기타 2편 |
| 인용 수정 | 13편 | 개정판을 가리키도록 인용만 바꿈 |
| 형식화 추가 | 6건 | Lean 형식화를 새로 더함(보조 결과 5건도 추가) |
오류를 누가 처음 찾았는지에 대해서는, OpenAI 대변인이 Retraction Watch에 “감사(audit) 중에” 찾았다고 말한 것이 확인된 전부예요. 연구 책임자 Dan Roberts는 X에 “6 new Lean formalizations, 19 modifications, and 3 withdrawals”(새 Lean 형식화 6건, 수정 19건, 철회 3건)라고 요약했어요. 이 수정 19건이 변경 기록의 증명 수정 14편, 인용 수정 13편과 어떻게 대응하는지는 공개 설명에 없어요. 그래도 회사가 정정 내역을 스스로 날짜별로 남겼기 때문에, 바깥에서도 무엇이 바뀌었는지 따라가 볼 수 있어요.
남은 원고 719편 가운데 증명이 맞는지 컴퓨터 프로그램으로 확인된 것은 42%이고, 나머지 58%는 수학자가 직접 읽어 확인해야 해요
변경 기록은 “300 / 719 = ~42%”라고 적었어요. 철회 뒤 남은 원고 719편 가운데 300편의 증명을 Lean으로 형식화했다는 뜻이에요. Lean은 증명을 컴퓨터가 읽을 수 있는 코드로 옮겨 적으면, 각 단계가 논리적으로 맞는지 프로그램이 검사해 주는 도구예요. 이 42%는 공개 다음 날 형식화 6건을 더한 뒤의 숫자예요. 공개 첫날 README는 형식화가 “Many, but not all”(많지만 전부는 아니다)이라고만 적었고, 비율은 적지 않았어요.
나머지 약 58%에는 기계 검증이 없어요. README도 “Some of the unformalized results could have issues”(형식화되지 않은 결과 가운데 일부에는 문제가 있을 수 있다)라고 스스로 적었어요. 대변인은 Retraction Watch에 결과의 “대략 50%”가 확인되지 않은 채 공개됐다고 말했는데, 저장소 숫자로 계산한 58%와는 맞지 않아요. 이 글은 저장소에 적힌 숫자를 따라요.
형식화를 마치기 전에 공개해도 되는지를 두고도 의견이 갈려요. 대변인은 IAS의 독립 자문단 AGMAI가 완전한 형식화를 기다리지 말고 공개하라고 권했다고 말했어요. AGMAI 권고문 4번은 형식화가 받아들일 수 없는 지연을 낳으면 형식화 상태를 분명히 밝히라고 적었어요. 그런데 같은 권고문은 첫 문단에서 AI 연구소가 내부 모델로 고급 수학 문제를 시험하는 관행을 지지하지 않는다고 했고, 결과는 AI 연구소가 통제하지 않는 저장소에 내라고 권했어요. OpenAI는 자사 GitHub에 원고를 냈고, 블로그에는 공동체가 운영하는 대안을 검토 중이라고 적었어요. Cornell의 Alex Townsend는 Lean으로 검증된 원고를 먼저 발표하고, 나머지는 따로 발표하면서 검증을 도와 달라고 했어야 한다고 말했어요.
Lean 검증이 원고의 증명을 그대로 보장하는지에 대해서는 다른 사례에서 반론이 나왔어요. Cambridge의 Anders Hansen 등 3명은, OpenAI가 9월에 별도 저장소로 낸 나비에-스토크스 증명에서 Lean 코드가 자연어 증명과 다른, 더 약한 진술을 증명한다고 주장했어요. 자연어 증명은 m+4번 미분을 다루는데 Lean 코드는 m+5번 미분을 다룬다는 예를 들었어요. 이번 719편을 분석한 논문은 아니에요. Hacker News에서는, 최종 명제를 Lean으로 옮길 때 쓴 정의는 사람이 미리 써 둔 것이라 최종 명제에는 문제가 없고 어긋난 곳은 중간 단계뿐이라는 반박도 올라와, 아직 논쟁 중이에요. 다만 프로그램이 검사하는 대상은 Lean으로 옮겨 적은 진술이에요. 그 진술이 원고에 쓰인 문장과 같은 내용인지는 결국 사람이 확인해야 해요.
수학자들은 이 원고들을 사람이 하나하나 읽어 확인하는 일이 자기 연구를 멈춰야 할 만큼 큰 부담이라고 했어요
Hansen은 New Scientist에 “대형 언어 모델이 만든 이 증명들은 모두 사람이 읽어야 하고, 이 일은 수학자들에게 엄청난 추가 부담을 지운다”고 말했어요.
집합론 연구자 Asaf Karagila는 자기 블로그의 ‘문제 목록’ 페이지에, 분할 원리(Partition Principle) 문제를 푼 사람에게 위스키 한 병을 보내겠다고 약속해 두었어요. 본인이 100년 넘은 문제라고 적은 이 문제를 OpenAI가 풀었다고 발표하자, 사람들이 그에게 샘 올트먼에게 위스키를 보낼 거냐고 물었어요. Karagila의 답은 “The answer to that is no”(답은 ‘아니요’다)였어요.
“I am trying to finish several papers, I am supervising a number of Ph.D. students, and I have a lot of active research of my own to do. When am I supposed to sift through a badly written paper?”(나는 논문 여러 편을 마무리하려 하고, 박사과정 학생 여럿을 지도하고, 내 연구도 많다. 잘 쓰이지 않은 논문을 언제 샅샅이 읽으라는 건가?) … “But it is the equivalent of a Denial of Service, should we want to take it seriously: stop everything else and figure this one out.”(진지하게 받아들이려 하면 이건 서비스 거부 공격과 같다. 다른 일을 모두 멈추고 이것부터 이해하라는 것이다.) (Asaf Karagila)
다만 Karagila는 Lean 코드는 보지 않았다고 밝혔어요. 그가 비판한 것은 원고의 글쓰기 품질이고, 증명이 틀렸다고 주장하지는 않았어요. AI 사용 자체에 반대하지 않는다고도 적었어요.
Terence Tao(UCLA)는 같은 부담을 수학 공동체 쪽에서 봤어요. 예전에는 큰 증명 하나가 나오면 강연·워크숍·협업이 뒤따르면서 여러 수학자가 그 증명을 이해하게 됐어요. 그런데 AI로 문제를 푼 사람들은 결과를 충분히 이해하지 못해 질문에 답하거나 강연을 하지 못하고, 그래서 세미나와 협업이 훨씬 적게 생긴다고 그는 지적했어요.
더 강하게 반대하는 쪽도 있어요. Association for Human Mathematics는 10월 7일 성명에서 “Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power”(700개 넘는 파일을 한 번에 내놓은 것은 학문을 보여 준 것이 아니라 힘을 과시한 것이다)라고 했고, 수학자들에게 OpenAI와의 협업을 멈추라고 촉구했어요. MIT의 Andrew Sutherland는 빠른 철회를 “the responsible thing to do”(책임 있는 행동)라고 평가하면서도, 잃은 신뢰를 되찾으려면 훨씬 더 많은 것이 필요하다고 했어요.
이번 공개를 반기는 쪽도 부담이 크다는 점은 인정해요. 토론토대의 Dan Litt는 Fortune에 “this is great for mathematics”(수학에 아주 좋은 일)라고 말했어요. 동시에 이 결과에서 이해를 끌어내려면 엄청난 양의 인간 노동이 들 것이고, 다만 그 노동은 수학자들이 늘 해 온 노동과 크게 다르지 않다고 했어요. OpenAI 안에는 모든 증명을 이해할 만큼 여러 분야의 수학자가 충분하지 않다고도 봤어요.
AI가 결과를 한꺼번에 쏟아내자, 수학에서 모자란 것이 증명을 만드는 힘에서 증명을 읽고 확인하고 책임질 사람으로 바뀌고 있어요
이번 공개 자료에서 빠진 숫자는 사람이 원고 1편을 읽고 확인하는 데 드는 시간이에요. 이 숫자는 OpenAI 자료에도, 비판한 수학자들의 글에도 없어요. 반면 증명을 만드는 쪽의 비용은 문제 약 4,000개, 결과 하나에 ChatGPT Pro가 평균 3시간 동안 생각하는 데 드는 연산이라는 숫자로 공개됐어요. 확인하는 쪽에서 공개된 숫자는 프로그램이 검사한 300편뿐이고, 나머지 419편은 수학자들이 시간을 내야 확인돼요.
| 증명을 만드는 쪽 | 증명을 확인하는 쪽 | |
|---|---|---|
| 공개된 숫자 | 문제 약 4,000개, 결과당 평균 약 3시간(ChatGPT Pro가 생각하는 시간으로 환산), 원고 722편 | Lean 형식화 300/719(약 42%) |
| 공개되지 않은 것 | 실패한 문제 수, 구체적인 선정 기준 | 사람이 원고 1편을 읽는 데 드는 시간 |
| 맡는 주체 | OpenAI 내부 모델 | 프로그램(42%)과 수학자(58%) |
공개 다음 날 원고 3편이 철회되고, 다른 원고 14편의 증명이 고쳐졌어요. Townsend는 오류가 더 나올 것이라고 봤어요. 변경 기록이 버전 노트와 철회본 보관 링크를 갖춘 것을 두고, Hacker News의 한 사용자는 “This is what it looks like when software engineering practices meet mathematics”(소프트웨어 개발 방식이 수학을 만나면 이렇게 된다)라고 적었어요. 원고가 먼저 나오고, 확인과 수정은 공개된 뒤에 따라오는 순서예요.
Tao가 제안한 “Math 2.0”은 이 변화에 대한 한 가지 답이에요. 그는 문제 풀이를 수학의 중심 자리에서 내려놓고, 결과를 풀어 설명하는 해설과 공동체를 만드는 일을 더 높이 평가해야 한다고 했어요. OpenAI도 블로그에서 앞으로 워크숍과 학회 비용을 대겠다고 적었어요. 증명 하나를 만드는 비용은 연산량으로 공개됐지만, 그 증명을 읽고, 틀린 곳을 찾아 철회하고, 질문에 답하는 일은 여전히 수학자 한 사람 한 사람의 시간으로 채워야 해요.
예전 수학은 어려운 문제를 풀어 증명을 만들어 내는 힘을 가장 높이 쳤어요. AI가 원고 722편을 한꺼번에 내놓자, 만들어진 원고의 절반 넘게가 사람이 읽어 확인하기를 기다리게 됐어요. 이제 수학이 집중할 곳은 증명을 읽어 확인하고, 다른 수학자에게 풀어 설명하고, 틀린 곳이 나오면 책임지는 일이에요.



