나비에–스토크스와 Lean 증명: 강제항 특이점과 실험실의 불투명성

2026년 9월 8일 OpenAI는 일반에 배포하지 않은 자사 내부 모델이 3차원 비압축성 나비에–스토크스 방정식에 대해 유한 시간 폭발(blowup)의 증명을 만들어냈다고 밝혔다. 회사는 이론 문서와 함께 공개 저장소 NavierStokesAndEuler를 내놓았다. 여기에는 외부 강제항이 작용하는 매끄러운 초기 데이터에 관한 정리들을 Lean 4 언어로 형식화한 내용이 담겨 있다. 연구소 측 설명에 따르면 이 결과는 수학자 찰스 페퍼먼이 클레이 수학연구소를 위해 작성한 문제 서술 가운데 정칙성 붕괴에 해당하는 명제들을 다룬다. 다만 외력이 없는 경우는 건드리지 않았는데, 학계는 바로 그 쪽이 이 문제의 더 어려운 변형이라고 본다. 공식 서술의 작성자는 이번 해결을 흥미진진하다고 평하며 코르도바와 마르티네스-소로아의 기여를 언급했고, 회사는 처음부터 100만 달러의 상금을 청구할 뜻이 없다고 분명히 했다.

이 사안은 수학의 자동화와 학술 기관의 시간을 한데 얽어놓는다. 클레이 수학연구소는 여전히 나비에–스토크스를 미해결 문제로 올려두고 있다. 규정은 자격 있는 지면에서의 발표, 발표 후 최소 2년의 대기, 그리고 수학계의 일반적 수용을 요구하며, 연구소는 아직 내용에 대해 입장을 내지 않았다. 마틴 브리드슨 소장은 절대적 엄밀성을 보장하기 위해 평가가 일부러 서두르지 않는 속도로 진행된다고 상기시켰다. 여기에 우선권 논쟁이 더해져 그림은 한층 복잡해졌다. 수학자 테런스 타오가 소개한 병행 연구가 있고, 저자들 스스로 그것이 인공지능의 도움을 크게 받았다고 설명한다. 뉴욕대의 한 수학자는 연구소가 제시한 접촉 경위 설명에 이의를 제기하며, 독점 도구의 비공개 세션이 결과에 기여했을 가능성을 제기했다. 회사는 미발표 연구를 직접 본 적이 없다고 부인하면서도, 비식별화된 사용 데이터가 자사 모델 학습에 영향을 주었을 가능성은 배제할 수 없다고 인정했다.

저장소에는 증명을 기계로 재검사하게 하는 지침이 들어 있지만, 지금까지 완료된 독립 검증은 없다. 그 검사를 제외하면, 사용된 인프라가 독점적이라는 사실이 비용과 과시된 효율 지표에 대한 모든 독립 검증을 가로막는다. 발표된 연산 규모 — 9월 1일부터 5일 사이 약 1만 개의 에이전트를 동시에 돌려 증명에 이르기까지 88시간, 형식화와 Lean 검증에 다시 17시간 — 는 외부에서 누구도 재현할 수 없는 회사 측 주장에 머문다. 학습 코드에도 시스템 가중치에도 접근할 수 없는 이상, 학계가 확인할 수 있는 것은 저장소에 올라온 형식적 단계뿐이며, 실험의 실제 재현 조건은 그늘에 남는다.

형식 수학은 논리 단계의 자동 검사라는 강력한 동맹을 얻었다. 그러나 닫힌 모델을 통한 과학적 선점 경쟁은 구조적 한계를 드러낸다. 정리를 검증하는 일은 이제 기계가 수행할 수 있는 작업이다. 그것을 만들어낸 공정의 투명성을 확인하는 일은 여전히 온전히 인간적인 엄밀성을 요구한다.

— Olya