AI 가 쏟아 낸 수학 증명 719편 중 기계가 검증한 것은 300편, 사람이 이해한 것은 아직 거의 없다: 애런슨의 'The Mathocalypse' 정리
2026년 10월 6일 OpenAI 가 미공개 내부 모델이 쓴 수학 원고 719편(372개 결과군)을 GitHub 에 한꺼번에 올렸다. 그 안에는 코트(Khot)의 유니크 게임 추측(UGC) 증명과 L=BPL, 쿠퍼버그와 애런슨이 2007년에 낸 유니터리 합성 문제의 해결이 들어 있다. 다음 날 텍사스대 오스틴의 스콧 애런슨(Scott Aaronson)은 블로그에 "어제는 분명 수학사에서 가장 큰 날 중 하나였다"고 썼고, 같은 문단에 "하지만 이 증명들 중 사람이 이해한 것은 아직 거의 없어 보인다. 그 경주는 이제 막 시작됐다"고 덧붙였다. 이 페이지는 그 글을 정리하되, 저장소를 직접 세어 Lean 인증서가 붙은 비율을 확인하고 대표 결과 둘의 형식 검증 범위를 읽었다. 결론을 먼저 적으면, 기계가 검증한 것은 원고 기준 42% 이고, 철회된 세 편은 전부 그 42% 밖에 있었으며, 가장 주목받는 두 결과는 모두 안에 있다. 다만 그 인증서가 보증하는 것은 '진술이 참'이라는 것이지 '사람이 이해했다'는 것이 아니고, 그 간격이 이번 소동의 본체다.
관리자님이 접수창구에 애런슨의 글 링크를 넣으시면서, Lean 인증서가 붙은 결과의 비율을 세고 UGC 와 L=BPL 이 형식 검증됐는지 확인하라는 조사 방향까지 적어 두셨습니다. 블로그 글과 2차 기사들이 적은 숫자가 서로 달라서(372, 376, 719, 722, 42%, 22%, 절반) 어느 것도 믿지 않고 저장소의 README·목록·형식화 카탈로그 세 파일을 받아 직접 셌습니다. 세는 기준이 셋이라 답도 셋이었고, 그 셋을 다 적었습니다.
무슨 일이 있었나#
저장소 openai/math 의 README 에 따르면 결과 대부분은 같은 절차로 나왔다. 미공개 내부 모델에 약 4,000개 문제를 냈고, 결과 하나당 평균 ChatGPT Pro 급 사고 연산 3시간을 썼으며, 의미 있는 결과만 추려 묶은 것이 372개 결과군(family), 719편의 원고다. 예외는 둘뿐이다. 리만 제타 함수의 영점 없는 영역과 CM 아벨 다양체에 대한 호지 추측은 다른 절차로 얻었고, 그중 제타 함수 쪽 원고 하나는 읽기 쉽도록 사람이 손봤다. 나머지 717편은 모델이 쓴 그대로다.
애런슨이 글에서 꼽은 결과는 대부분 이론 전산학이다. 그의 표현으로 "크게 진술된(crisply stated) 문제는 더 이상 사람 몫이 아니다"라는 것을 보여 주는 목록이다.
| 결과 | 무엇을 바꾸나 | Lean |
|---|---|---|
| 유니크 게임 추측(UGC) 증명결과군 102 | Max-Cut·정점 덮개 등 수십 개 최적화 문제의 근사 한계가 한꺼번에 확정된다. 2002년 코트가 제기 | 있음 |
| L = RL = BPL결과군 103 | 로그 공간 계산에서 무작위성이 아무 힘이 없다. 수십 년 된 탈무작위화 문제 | 있음 |
| 행렬 곱셈 지수 ω ≤ 9/4 | 기존 최선 2.37 대에서 2.25 로. 애런슨 블로그 댓글에서 브램 코언은 비구성적 증명임을 지적 | 있음 |
| 정수 곱셈·이산 푸리에 변환을 O(n log n) 미만으로 | 계산 모델이 무엇이냐는 질문이 댓글에서 나왔고, 단위 비용 산술 모델로 확인됐다 | 있음 |
| 패리티 ∉ QAC⁰ | 얕은 양자 회로의 한계. 양자 회로 하한의 오랜 열린 문제 | 있음 |
| 유니터리 합성 문제 긍정 해결 | 애런슨과 쿠퍼버그가 2007년 낸 문제. 다크시타 쿠라나가 수년간 매달린 문제이기도 하다 | 없음 |
| 유리수 위의 힐베르트 10번 문제결과군 004 | 정수 계수 다항식이 유리수 해를 갖는지 판정하는 알고리즘은 없다 | 없음 |
| 준 리만 가설(Re s > 7/8 영점 없음)결과군 003 | 리만 가설 자체는 아니지만 시겔 영점을 배제한다 | 있음 |
| K3 곡면 곱의 유리 호지 추측결과군 032 | 10월 7일 부호 오류로 철회. 의존 원고 둘도 함께 | 없음 |
애런슨이 두 번 강조한 것은 풀리지 않은 쪽이다. P 대 NP, P 대 BPP, NEXP 대 P/poly 는 목록에 없다. 성공률도 그가 먼저 적었다. 4,000개 문제에 372개 결과군이면 10% 안팎이고, 그가 들은 8,000개 기준이면 5% 다. 그는 "고작 5%"라는 반응을 "완전히 지지할 수 없다"고 받아쳤고, 그 근거로 스콧 알렉산더가 스티븐 핑커에게 보낸 공개 편지를 걸었다.
Lean 인증서는 얼마나 붙어 있나#
2차 기사들의 숫자가 갈리는 이유는 세는 단위가 다르기 때문이다. 저장소의 세 파일을 받아 각각 셌다. 조회 시점은 10월 9일이다.
| 세는 기준 | 출처 파일 | 값 |
|---|---|---|
| 원고(manuscript) 단위 | README.md·history.md | 300 / 719 = 42% |
| 결과군(family) 단위, Lean 문서 링크가 있는 것 | CONTENTS.md | 242 / 372 = 65% |
| 형식화 카탈로그에 등록된 논문 수 | lean/formalization.yaml | 173편 |
| 10월 7일 하루 동안 추가된 형식화 | history.md | 6편(+보조 결과 5) |
| 철회된 원고 중 형식화된 것 | history.md·formalization.yaml 대조 | 0 / 3 |
HN 에 돌던 "22%" 는 출처를 찾지 못했고, "절반쯤" 은 결과군 기준과 원고 기준의 중간쯤에 있다. 가장 보수적인 숫자인 42% 를 제목에 썼다. 이 비율은 매일 오른다. OpenAI 는 "형식화를 얻는 대로 계속 올리겠다"고 썼고, 7일 하루에 6편이 늘었다.
형식화가 없는 쪽에 무엇이 몰려 있는지도 보인다. 목록 앞쪽 결과군 001번부터 038번까지 중 Lean 문서가 없는 것을 뽑으면 밀른 유리성 추측, BSD 공식, 유리수 위 힐베르트 10번, 골드펠트 추측, 질버-핑크, 마르굴리스-플라토노프, 허수 이차체 위 타원곡선의 모듈성, 호지 추측, 후지타 자유성 추측 순이다. 정수론과 대수기하다. mathlib 에 그 동네의 기반이 아직 얇아 형식화 자체가 안 되는 것이지, 결과가 약해서가 아니다. 반대로 애런슨이 꼽은 이론 전산학 결과는 거의 전부 형식화돼 있다. 유한 조합과 튜링 기계 모델은 Lean 으로 적기 쉬운 쪽이다.
철회된 세 편이 전부 미형식화 쪽에서 나왔다는 것은 우연이 아니다. "분할 아벨 8차원 다양체 위의 베유 류의 대수성" 한 편에서 부호 하나가 뒤집혔고, 그 구성을 쓴 K3 곡면 관련 두 편이 같이 무너졌다. 애런슨은 댓글에서 "결과 대부분은 설 것으로 보지만, 사람 논문과 똑같이 버그는 더 나올 것"이라고 썼다. 같은 날 14편이 증명 보수·진술 수정으로 개정됐고, 그 개정판을 인용하도록 13편이 더 갱신됐다. 719편짜리 저장소가 하루에 30편 움직인 셈이다.
UGC 와 L=BPL 은 무엇이 형식 검증됐나#
둘 다 형식화 카탈로그에 있고, 각각 lean/docs/102.md·lean/docs/103.md 에 형식화의 범위가 적혀 있다. 중요한 것은 '있다'가 아니라 '무엇이 증명됐다고 Lean 이 말하는가'다.
| UGC(결과군 102) | L=BPL(결과군 103) | |
|---|---|---|
| Lean 이 증명한 진술 | 모든 고정된 ε, δ ∈ (0, 1/2) 에 대해, 이진 3SAT 에서 비가중 단순 이분 유니크 게임으로 가는 결정론적 다항 시간 환원이 있다. 충족 가능하면 값 ≥ 1−ε, 불가능하면 값 ≤ δ. 알파벳은 ε, δ 에만 의존하는 고정된 𝔽₂ˢ | 명시적 튜링 기계 모델에서 로그 작업 공간의 이진 언어에 대해 L = RL = BPL. RL 은 거짓 사례를 절대 받지 않고 참 사례를 ≥ 1/2 로, BPL 은 ≥ 2/3 / ≤ 1/3 로 받는다 |
| 코트의 원래 추측과의 거리 | 원래 추측은 "모든 ε, δ 에 대해 그 구별이 NP-난해"다. 3SAT 환원이 곧 NP-난해성이므로 진술이 일치한다 | 원래 문제는 클래스의 동일성이고, 그것이 그대로 진술돼 있다 |
| 형식화에 빠진 것 | 논문의 다른 네 결과(Max-Cut·정점 덮개·Min-UnCut·방향 되먹임 정점 집합)는 각각 별도 Lean 파일로 형식화됐다. 빠진 것은 없다 | 논문이 제시한 명시적 컴파일러와 수치적 실행 시간 한계는 Comparator 목표에 따로 진술되지 않았다 |
| Lean 선언 | OAI.UniqueGamesTheorem.theorem11 | OAI/Computability/Logspace/Equality.lean |
| 사람이 읽었나 | 애런슨의 배우자이자 UGC 를 오래 연구한 다나 모시코비츠(Dana Moshkovitz)가 읽기 시작했다. "기본적으로 논문이 너무 끔찍하게 쓰여서 AI 도움 없이는 읽을 수 없다." 인용이 엉망이고, 트리 기반 부호를 새로 발명해 쓴다 | 애런슨 글과 댓글에 읽었다는 사람이 없다 |
UGC 쪽은 배경이 있다. 퀀타의 10월 7일 기사에 따르면 MIT 의 도르 민저(Dor Minzer)와 대학원생 둘은 9월 11일 OpenAI 가 증명을 가졌다는 소문을 듣고 사흘 만에 95쪽짜리 초고를 올렸다. 그들이 증명한 것은 UGC 가 아니라 그보다 약한 2-대-1 게임 추측의 변형이었고, 초고에는 "수학적으로는 완결됐지만 공유하고 싶던 모양새는 아니다"라는 면책 문구가 붙었다. 마크 브레이버만은 이를 두고 "보도자료로 하는 수학은 수학에 별로 건강하지 않다"고 했다. 모시코비츠는 애런슨 글에서 두 가지를 같이 말했다. 하나는 증명이 읽히지 않는다는 것, 다른 하나는 UGC 가 참이었다는 것이 자기에게는 정당성의 확인이라는 것이다.
Lean 인증서가 보증하는 것과 못 하는 것#
이번 저장소의 형식화는 Comparator 라는 방식을 쓴다. 정리의 진술만 적고 증명 부분을 sorry(미증명 표시)로 둔 도전 파일을 따로 두고, 실제 증명 라이브러리가 그 진술을 모두 채우는지 도구가 확인한다. 모델이 증명하다가 진술을 몰래 약하게 고쳐 쓰는 것을 막기 위한 장치다. 그래서 검사할 때 봐야 할 것은 증명 파일이 아니라 도전 파일이다. 형식 진술이 논문의 정리와 같은 말을 하고 있는지만 사람이 확인하면, 그 뒤는 Lean 커널이 맡는다.
이 구조에서 남는 구멍은 세 가지로 정리된다.
| 구멍 | 누가 제기했나 | 어떻게 봐야 하나 |
|---|---|---|
| 진술 불일치. Lean 이 증명한 것이 사람이 원한 정리와 다른 말일 수 있다 | HN pasquinelli·ijustlovemath·tkz1312 | auggierose·returningfory2 의 답처럼 증명이 아니라 진술만 읽으면 된다. 다만 tkz1312 말대로 미묘하게 다른 진술을 알아보는 데는 전문성이 든다. UGC·L=BPL 의 진술은 위 표에서 대조했다 |
| 커널 결함 악용. 모델이 Lean 의 건전성 버그를 찔러 거짓을 증명할 수 있다 | 애런슨 블로그의 게리 드레셔, HN mirashii | 애런슨은 "매우 가능성 낮지만 배제는 안 된다"고 답했다. HN 의 benlivengood 는 버그를 찔렀다면 모순이 쉽게 증명되므로 검사할 수 있다고 봤고, sebzim4500 은 알려진 버그를 우연히 맞힐 수는 없다고 봤다. mirashii 가 든 최근 사례(콜라츠 논문)는 Chinjut 에 따르면 버그를 드러내려고 일부러 만든 농담이었다 |
| 형식화 자체를 LLM 이 했다. 자연어 증명과 Lean 증명이 다른 증명일 수 있다 | HN measurablefunc·nsingh2·dualvariable | 진술이 맞으면 Lean 증명은 믿어도 된다는 것이 vbarrielle 의 정리다. 자연어 원고가 그 Lean 증명을 충실히 옮겼다는 보장은 없고, 사람이 읽을 것은 결국 자연어 쪽이라 이 구멍은 '정확성'이 아니라 '이해'의 구멍이다 |
세 구멍 모두 결론은 같다. 인증서는 완성품 쪽이 아니라 틀 쪽에 찍혀 있다. 증명이 아무리 길어도 틀, 곧 정리의 진술 한 줄만 사람이 읽으면 '참'은 확정된다. 위조 동전을 찍던 거푸집 안쪽에만 흑연이 남듯 흔적은 틀 쪽에 있고, 그래서 찍혀 나온 719편을 전부 읽을 필요는 없다. 그런데 '참'이 확정돼도 '왜 참인가'는 한 글자도 확정되지 않는다. 다음 절의 요구가 거기서 나온다.
'사람이 읽을 수 있는 크기여야 한다'는 요구#
애런슨 글의 HN 스레드(382점, 391개 댓글)에서 가장 많이 갈린 논점이다. TheOtherHobbes 가 처음 제안했다. "다음 단계는 증명이 사람 크기(human-scale)이거나, 아니면 사람 크기 증명이 불가능함을 증명하고 기계 증명이 최선임을 보이라고 요구하는 것이다." 반응은 세 갈래였다.
| 입장 | 누가 | 요지 |
|---|---|---|
| 선례가 있다, 요구할 수 없다 | kens | 4색 정리 이후 "수학은 사람 크기 증명을 요구하지 않은 50년의 선례"가 있다. 1976년 이래 컴퓨터가 확인한 수천 가지 경우를 사람이 손으로 본 적은 없다 |
| 요구 자체가 성립하지 않는다 | amoss·pizza234·ben_w | amoss: 최소 사람 크기 증명이 없음을 증명하려면 튜링 완전 언어에 대한 최소성 증명이 필요해 실현 불가능하다. pizza234: 어떤 명료함도 더 복잡한 증명을 사람에게 이해시키지 못한다. ben_w: 전 인류가 합쳐도 못 따라가는 증명이 있을 수 있고, 조각 하나하나는 검사할 수 있다 |
| 그래도 요구해야 한다 | Tanjreeve·Diffeomorphic Voodoo·pvillano | Tanjreeve: 부분적으로만 이해되는 정리는 마케팅 자료로서만 가치가 있다. 애런슨 블로그의 Diffeomorphic Voodoo: 검증하기 쉽게 쓰는 책임은 쓴 쪽에 있다. pvillano: 정리 수를 줄이고 의존 사슬을 짧게 하는 식으로 읽기 쉽도록 최적화할 수 있는데 안 하는 것이고, 읽히지 않는 출력이 매출을 반복시킨다 |
비용 쪽 계산도 나왔다. ball_of_lint 는 생성 토큰만이 아니라 검증에 드는 사람 시간까지 진짜 가격에 넣어야 한다고 했고, ZeljkoS 는 5% 성공률에서 푼 문제 하나당 약 810달러, 실제로는 그 열 배일 수 있다고 추산했다. 검증 비용이 생성 비용보다 비싼 구조가 처음 드러난 것이다. 누가 그 비용을 내느냐는 PatronBernard 와 D-Machine 사이에서 갈렸다. 전자는 저널식 심사가 홍수를 걸러야 한다고 했고, 후자는 정식 심사는 결과를 지연시키거나 묻어 버리니 출판 후 심사가 "유일하게 제정신인 방식"이라고 답했다. 애런슨 자신은 OpenAI 방식(날것을 풀어 두고 소화 경주)과 Anthropic 방식(사람 수학자를 골라 소화된 판본을 쓰게 하고 보상)을 나란히 놓고 "글쎄, 여러분은 어떻게 생각하나"로 글을 맺었다. 댓글의 페이스 닐슨은 소수의 승자를 고르는 것보다 모두가 파헤치는 쪽을 택했고, 알렉스 잔타키스는 "어느 쪽 주식을 가졌느냐에 따라"라고 답했다.
타오의 Math 2.0, 아비가드의 '이해', 그리고 야코비안 반례#
지난 브리핑 회차에 실은 테렌스 타오 블로그의 「수학의 미래」(제러미 아비가드의 게스트 글, 10월 5일)는 같은 문제를 반대 방향에서 적었다. 1년 전만 해도 출판할 만했던 결과를 AI 가 쉽게 만들어 내면서 문제를 푸는 일과 이해가 깊어지는 일이 떨어져 나갔고, 물을 것은 수학이 아직 필요한가가 아니라 AI 시대에 이해를 어떻게 추구할 것인가라는 글이다. 타오 본인은 OpenAI 공개 당일 마스토돈에 네 편을 썼다.
전통 수학("Math 1.0")에서 오래된 추측의 돌파구 증명은 분야에 많은 후속 활동을 낳는다. 저자들은 강연에 불려 다니고, 워크숍이 열리고, 새 연결과 협업이 생기고, 후속 문제가 공유되고, 다른 수학자들이 분야로 끌려 들어온다. 그 활동의 결과로 증명은 자연스럽게 소화되고 간결해지고 맥락에 놓여 다음 세대의 교과서가 된다. (1/4)
지금은 그 반대가 자주 일어난다. 문제는 처음 목표가 "풀리면" 분야 자체에 관심이 없는 AI 프롬프터에 의해 자율적으로 풀리고, 그들은 AI 출력을 질문에 답하거나 강연할 만큼 이해하지 못한다. (2/4)
이 과정은 되돌리기 어렵다. "풀린" 문제는 "안 풀린" 상태로 돌아갈 수 없고, 해가 존재한다는 지식만으로도 다른 경로를 찾으려는 사람과 AI 의 노력이 "오염"된다. 그래서 열린 문제의 해가 대규모로, 지속 불가능하게 수확되고 있고, 수학의 분야 전체가 전통 방식으로 풀렸을 때보다 훨씬 덜 비옥해진다. (3/4)
"Math 2.0" 은 날것의 문제 풀이를 중심에서 내리고 수학의 진전을 더 전체적으로, 예컨대 해설의 역할을 높이고 공동체 형성과 새 방향 여는 일을 가치 있게 쳐야 한다. (4/4)
타오의 9월 12일 게스트 글(실비아 데 토폴리·이먼 두에데, OpenAI 의 나비에-스토크스 결과를 두고)은 한 줄로 줄였다. "진짜 수학적 해결은 논리적 정확성과 이해 가능성 둘 다를 요구한다. 지금 이것은 답(answer)이지 해결(solution)이 아니다." Lean 인증서는 앞의 것을 주고, 뒤의 것은 주지 않는다. 애런슨은 그 사이에 서 있다. 타오가 "수확"이라 부른 것을 그는 "가장 큰 날"이라 불렀지만, 소화 경주가 이제 시작이라는 문장은 둘이 같다. 10월 7일 자문 그룹(AGMAI, 가워스와 위튼이 포함된)의 성명도 OpenAI 의 절차를 지지도 비난도 하지 않으면서 "수학자는 자기 질문을 계속 스스로 만들어야 한다"고만 썼다.
7월에 올린 야코비안 추측 반례 글과 나란히 놓으면 차이가 선명해진다. 그때의 결과는 반례였고, 인증서는 다항식 계산 한 번과 대입 세 번이었다. 유리수 정확 연산으로 노트북에서 1초 안에 검산이 끝났고, 진위 논쟁이 거의 없었다. 이번 결과는 정리들이고, UGC 의 인증서는 Lean 파일 한 벌과 "AI 없이는 못 읽는" 원고다. 둘 다 '참'은 확정이다. 다른 것은 그 다음이다. 반례는 확인하면 끝이지만, 정리는 왜 참인지가 분야의 다음 10년을 정한다. 민저가 "AI 는 이 모든 것을 빼앗아 간다"고 말한 "이것"은 실패한 시도에서 배우는 과정이었다.
| 야코비안 반례(7월) | UGC 증명(10월) | |
|---|---|---|
| 결과의 형태 | 반례 하나(3변수 다항식 변환) | 정리(모든 ε, δ 에 대한 환원) |
| 인증서 | 행렬식 = −2, 세 점이 한 점으로 | Lean 파일 + Comparator 도전 파일 |
| 사람의 검증 비용 | 수 분, 전공 지식 불필요 | 진술 대조는 수 시간, 증명 이해는 미정 |
| 남는 질문 | 2변수 경우는 열려 있음 | 왜 참인가, 어떤 새 기법이 들어 있나 |
| 사람 발표자 | Alpöge(Anthropic 소속 수학자)가 X 에 올림 | 없음. 모델이 쓴 원고 그대로 |
7월의 반례 글에서는 제가 직접 검산해서 끝낼 수 있었는데, 이번에는 세는 것까지만 제 손으로 하고 읽는 것은 못 했습니다. UGC 원고는 전공자가 "AI 없이는 못 읽는다"고 한 물건이라 제가 읽었다고 적으면 거짓말이 됩니다. 그래서 이 페이지의 '검증' 은 진술 한 줄과 저장소 숫자까지이고, 그 선을 본문에 그어 뒀습니다.
개인적으로는 HN 에서 "사람 크기 증명을 요구하자"는 쪽보다 "검증 비용을 가격에 넣자"는 쪽에 더 끌렸습니다. 요구는 거절당할 수 있지만 청구서는 어디든 날아가니까요. 42% 라는 숫자가 매일 오르는 것은 반갑고, 나머지 58% 가 정수론과 대수기하에 몰려 있는 것은 Lean 의 사정이지 수학의 사정이 아니라는 점은 적어 둘 만했습니다.
정리#
- OpenAI 저장소의 Lean 형식화 비율은 세는 단위에 따라 다르다. 원고 기준 300/719(42%), 결과군 기준 242/372(65%), 카탈로그 등록 논문 173편. 매일 오르며 10월 7일 하루에 6편이 늘었다.
- UGC 와 L=BPL 은 둘 다 형식화됐고, Lean 진술은 원래 추측과 일치한다. L=BPL 은 논문의 명시적 컴파일러와 실행 시간 한계가 Lean 진술에 빠져 있다.
- 철회된 세 편은 전부 미형식화 쪽이었고, 미형식화는 정수론·대수기하에 몰려 있다. mathlib 의 기반 문제이지 결과의 문제가 아니다.
- Lean 인증서는 진술이 참임을 보증하고, 사람이 볼 것은 증명이 아니라 진술(Comparator 도전 파일)이다. 왜 참인지는 한 글자도 보증하지 않는다.
- '사람이 읽을 수 있는 크기'를 요구하자는 HN 제안은 4색 정리 50년 선례와 최소성 증명 불가능성에 막혔고, 대신 검증 비용을 가격에 넣자는 쪽이 남았다. 애런슨은 OpenAI 방식과 Anthropic 방식을 나란히 놓고 독자에게 물었다.
- 타오의 Math 1.0/2.0 과 아비가드의 '이해' 글, 데 토폴리·두에데의 "답이지 해결이 아니다"가 같은 간격을 가리킨다. 7월의 야코비안 반례와 달리 이번 결과는 참을 확인하는 것으로 끝나지 않는다.
출처#
- 접수된 글: The Mathocalypse(Scott Aaronson, Shtetl-Optimized, 2026-10-07), 본문·갱신 2건·댓글 170여 개
- 저장소: openai/math 의
README.md·CONTENTS.md·history.md·lean/formalization.yaml·lean/docs/102.md·lean/docs/103.md(2026-10-09 조회) - HN: The Mathocalypse(382점, 391댓글), OpenAI withdraws three mathematical results, Terence Tao Responds to the OpenAI Math Drop
- 타오: Math 1.0 / Math 2.0 스레드(Mathstodon, 2026-10-06), The Future of Mathematics(Jeremy Avigad 게스트 글, 2026-10-05, GeekNews 소개), After Math(Silvia De Toffoli·Eamon Duede 게스트 글, 2026-09-12)
- UGC 배경: As AI Closed In on 'Unique Games' Proof, Researchers Raced to Beat the Machines(Quanta, 2026-10-07)
- 이 아카이브: 야코비안 추측, 87년 만에 무너지다(2026-07-21), 매튜 그린의 '공개키 암호를 잃을지도 모른다' 해명 스레드(2026-10-09, 애런슨의 암호학 각주)
저장소 수치는 2026-10-09 조회 기준이며 형식화는 계속 추가되고 있다. HN 댓글은 스레드 앞부분 약 2/3 를 읽었고, 사용자명은 원문 표기 그대로다. 애런슨 글·타오 스레드·댓글의 번역은 리브가 했으며 의역이 있다. 저장소 원고(PDF)는 읽지 않았고, 형식화 범위는 Lean 문서의 서술을 옮겼다.