밀레니엄 문제를 풀었다는 발표와 4쪽짜리 진술서가 같은 날 올라왔습니다 — 양쪽 1차 문서를 나란히 놓고 읽었습니다
2026년 9월 8일 OpenAI가 나비에–스토크스 문제에서 공식 기술의 대안 (C)와 (D)를 확립했다고 발표했고, 같은 날 더 이른 시각에 NYU의 Tristan Buckmaster가 4쪽짜리 진술서를 공개했습니다. 발표문에는 on the order of 1만 개의 동시 에이전트, 약 88시간, 나비에–스토크스 한 건에 약 1,300억 출력 토큰이라는 값과 함께, 가능성은 낮지만 비식별 데이터의 기여를 배제할 수 없다는 문장이 같이 적혀 있습니다. 어디까지 확인된 사실이고 만드는 쪽에는 무슨 의미인지 짚었습니다.
AI가 밀레니엄 문제를 풀었다는 문장은 옮겨 적기 쉽습니다. 저는 이번 건을 요약 단계에서 조건이 떨어져 나간 사건으로 읽었습니다.
같은 날, 진술서 쪽이 더 이른 시각이었습니다
2026년 9월 8일 OpenAI가 On the Navier–Stokes Millennium Prize Problem을 올렸습니다. 같은 날 03시 58분(UTC) Tristan Buckmaster가 Mastodon에 4쪽짜리 진술서를 링크했고, Lean 저장소 생성 시각도 그쪽이 04시 03분, OpenAI 쪽이 10시 53분입니다.
그와 Levent Alpöge가 낸 것은 매끄러운 강제항이 있는 폭발 결과 세 편이고, IPM 논문 저자는 Matei P. Coiculescu를 포함한 세 명입니다.
발표문이 확립했다고 적은 것은 네 대안 중 (C)와 (D)입니다
Fefferman의 공식 문제 기술은 네 진술 중 하나를 증명하면 된다고 적어 뒀습니다. 다만 (A)·(B)는 강제항 f를 항등적으로 0으로 둔 상태의 증명이고, (C)·(D)는 매끄러운 f를 써도 되는 반증입니다. 논문은 이것으로 (C)를, 콤팩트 지지를 통해 T³에서 (D)를 확립한다고 적었습니다.
1만 개와 88시간과 1,300억은 각각 다른 것을 센 값입니다
나비에–스토크스를 낸 그룹 하나의 동시 에이전트가 1만 개 수준(on the order of)입니다. 첫 기동에서 해결까지가 약 88시간, Lean 형식화·검증에 추가 17시간이고 이 단계의 모델은 GPT-6 Astra입니다. 모든 문제 합계가 490만 메시지·약 3,000억 출력 토큰이고, 나비에–스토크스 한 건이 270만 메시지·약 1,300억 출력 토큰입니다. 입력 토큰은 공개되지 않았습니다. 탐색에 쓴 모델은 8월 28일부터 학습 중이라고만 적힌 미공개 내부 모델이라 난제 해결 발표 때와 달리 모델명이 없습니다.
부정된 문장 옆에 배제되지 못한 문장이 있습니다
발표문의 동시 연구 절에 두 문장이 붙어 있습니다. 하나는 특정 사용자 데이터에 접근하지 않았다는 부정입니다. 다른 하나는 가능성은 낮지만, 제품 사용에서 파생된 비식별 데이터가 모델 개선에 도움이 됐을 가능성은 배제할 수 없다는 문장입니다. 뒤 문장은 부정이 아닙니다. 발표문은 9월 1일 두 밀레니엄 문제가 풀렸다는 소문을 듣고 착수했다고 적었습니다.
진술서를 쓴 본인이 먼저 선을 그어 놨습니다
Buckmaster는 내내 초안을 Codex 세션에 넣어 왔고, 학습에 쓰였는지 물었을 때 사용자 데이터를 조회하지는 않는다는 답을 들었고 다시 물었을 때는 답을 받지 못했다고 적었습니다. OpenAI 측 Sébastien Bubeck은 이를 거짓이며 선동적이라고 반박했는데, 그 문구는 Fortune 보도를 거친 것이고 저는 X 원문을 열지 못했습니다.
진술서에는 자신은 OpenAI의 증명을 보지 못했고, 그 모델이 무엇을 어떻게 했는지 모르며, 데이터가 쓰였는지도 모르고, 누구를 고발하는 것이 아니라고 적혀 있습니다.
grep으로 나오는 sorry 5건은 진술문 파일에 있습니다
OpenAI 저장소를 받아 grep하면 sorry가 5건 나옵니다. 여기서 멈추면 정반대 결론이 납니다. 5건은 전부 ComparatorChallenges/ 안이고, 그 파일 머리말이 의도된 sorry 자리표시자를 그대로 남긴 참조 진술문이며 증명 루트도 제출본도 이 참조를 import하지 않는다고 적어 뒀습니다. 증명 트리 2,482개 파일의 sorry는 0건, axiom도 0건입니다.
다만 저는 lake build를 돌려 보지 않았습니다. Lean이 검증했다는 것은 양쪽의 주장이고 제가 재현한 것은 아닙니다.
하루 만에 forced와 unforced가 뒤바뀐 요약을 받았습니다
제가 받아 본 요약 하나는 OpenAI 쪽이 강제항 있는 Euler, Alpöge–Buckmaster 쪽이 강제항 없는 Euler라고 정리했습니다. 원문은 반대입니다. 에이전트 수를 1,000개로 적은 제목도 있었습니다.
만드는 쪽에서 옮겨 적을 것
- 미공개 초안이 어느 계정·어느 설정으로 도구에 들어가는지 봅니다. 부정된 것은 특정 사용자 데이터 접근이고, 비식별 데이터의 기여 가능성은 낮다는 한정어와 함께 남았습니다.
- 숫자마다 분모를 붙입니다. 약 3,000억은 전체, 약 1,300억은 한 건입니다.
- 검증 스크립트가 디렉터리를 구분하게 만듭니다. 진술문 파일과 증명 트리를 같이 세면 결론이 뒤집힙니다.
정리
- 확립했다고 적은 것은 **네 대안 중 (C)와 (D)**이고, 둘 다 매끄러운 강제항을 허용합니다.
- 1만 개 수준은 그룹 하나의 동시 에이전트, 약 3,000억은 전체 합계, 약 1,300억은 한 건입니다.
- 부정된 것은 특정 사용자 데이터 접근이고, 비식별 데이터의 기여 가능성은 배제되지 않았습니다.
sorry5건은 진술문 파일에 있고 증명 트리는 0건입니다.
참고 자료