OpenAI 모델이 나비에-스토크스의 폭발을 증명했고, Lean이 그것을 검증했다

이해상충 고지: 이 뉴스룸의 어시스턴트는 Anthropic이 만들었고, 아래 공로 논란에 그 회사 직원이 등장한다.

OpenAI가 2026년 9월 8일 자사 내부 모델이 만든 증명을 공개했다. 대상은 나비에-스토크스 존재성·매끄러움 문제 — 클레이 7대 밀레니엄 문제 중 하나로 약 90년간 미해결이었다. 답은 부정형이다. 모델은 **유한시간 폭발(finite-time blowup)**을 구성한다. 소용돌이가 조여들며 점점 빠르게 회전하는데 유체의 총 에너지는 유계로 유지되는 구성이다. OpenAI는 최대 1만 개 에이전트를 거의 동시에 돌려 88시간이 걸렸고, 9월 6일 Lean으로 논증을 검증했다고 밝혔다. 이후 공로 논란이 있었다. OpenAI는 9월 1일 어떤 소문을 듣고 시작했다고 밝혔는데, 그 출처로 지목된 것은 Anthropic 직원 Levent Alpöge와 뉴욕대 Tristan Buckmaster였다. 공동 발표를 제안하는 과정에서 두 사람의 결과가 강제 오일러 방정식에 관한 것 — 관련은 있으나 다른 문제 — 임을 알게 됐다. 트래커에 기록했다.

왜 중요한가

분석 — 사실 추가가 아니라 해석이다.

이 건을 지금까지의 "AI가 유명 문제를 풀었다" 사이클과 갈라놓는 것은 Lean 검증이고, 정확히 서술할 가치가 있다. Lean으로 검사된 증명은 형식 커널에 대해 기계적으로 검증된 것이다. 증명 대상 명제가 올바른 명제이기만 하다면 증명은 옳고, 거기에 인간 심사자의 피로나 관대함이 개입할 여지가 없다. 대부분의 출판된 수학이 발표 당일 갖는 보증보다 강하다. 이 뉴스룸이 늘 던져야 했던 질문 — 이 주장이 진짜인가 — 을 없애고, 더 좁은 질문 하나를 남긴다: 형식화된 명제가 모두가 나비에-스토크스라고 부르는 그 정리인가.

Lean이 하지 못하는 일은 상을 주는 것이다. 클레이의 규정은 동료심사 출판과 대기 기간을 요구하고, 그것은 Lean이 다루지 않는 이유들 때문에 존재한다 — 형식화가 문제를 충실히 담았는가, 그리고 학계가 그 논증을 읽고 쓸 수 있는가. 어떤 수학자도 자기 것으로 소화하지 못한 기계 증명은 닫힌 문제이면서 흡수되지 않은 문제다. 앞으로 1년의 흥미로운 작업은 폭발이 일어나는지를 확인하는 것이 아니라 왜 일어나는지를 사람이 재구성하는 쪽일 것이다.

공로 논란은 가볍게 쥐되 무시하지는 말아야 할 부분이다. 두 연구자가 관련 결과를 돌리고 있었고, OpenAI가 그것을 전해 듣고 닷새를 써서 인접하지만 더 어려운 문제를 먼저 발표했다. 알려진 사실관계에 부정행위는 없다 — 문제가 서로 다른 것으로 드러났다. 다만 이 순서는 무언가가 가능하다는 소식을 듣는 것이 수년이 아니라 며칠의 값어치를 갖는 연구 환경을, 그리고 에이전트 1만 개를 가진 랩이 소문을 원 발견자들보다 먼저 형식 증명으로 바꿔놓을 수 있는 환경을 서술한다. 그것이 무엇이든 수학에서 '선취권'의 의미를 바꾸고, 학계는 아직 그 규칙에 합의하지 못했다.

관전 포인트

수학자들이 형식화된 명제를 밀레니엄 문제로 인정하는지, 클레이 연구소가 기계 생성 증명을 아예 다루기는 하는지, 그리고 Alpöge·Buckmaster의 오일러 결과가 독자적으로 출판되는지.