OpenAI의 AI가 자신의 Navier-Stokes 수학 증명을 코드로 오역

OpenAI가 발표한 것

OpenAI는 2026년 9월 8일, 내부 멀티에이전트 시스템이 Navier-Stokes 존재성 및 평활성 문제를 해결하는 증명을 생성했다고 말했습니다. 이는 Clay Mathematics Institute의 100만 달러 상금을 받는 7개의 밀레니엄 상 문제 중 하나입니다. AI 추적 사이트 implicator.ai에 따르면, 회사는 약 10,000개의 에이전트가 8월 28일부터 88시간 동안 작업하여 270만 개의 에이전트 메시지와 약 1,300억 개의 출력 토큰을 생성한 후, GPT-6 Astra로 설명되는 별도의 모델이 증명 언어 Lean에서 논증을 형식적으로 검증하는 데 17시간을 더 보냈다고 보도했습니다.

결과는 "Finite time blowup for Navier–Stokes"라는 제목의 자연 언어 원고와 컴퓨터가 모든 논리적 단계를 확인할 수 있도록 하는 Lean 프로젝트였습니다. 이는 implicator.ai 및 나중에 작업을 분석한 arXiv 논문에 기술되어 있습니다.

번역 오류 발견

프리프린트 서버 arXiv에 게시된 "Navier-Stokes Lost in Translation"이라는 제목의 논문은 수학자 Alexander Bastounis, Fabian Circelli, Anders C. Hansen에 의해 작성되었으며, OpenAI의 Lean 코드가 실제로 자연 언어 논문의 수학적 논의와 일치하는지 여부를 조사했습니다. 저자들은 단순히 컴파일되는 Lean 증명과 원래의 추론에 의미적으로 충실한 증명의 차이를 구분하며, 두 번째 유형이 첫 번째 유형보다 보장하기가 훨씬 더 어렵다고 주장합니다.

논문은 구체적인 불일치를 나열합니다. 한 경우, 자연 언어 논문의 Lemma 8.6은 4개의 추가 입력 차수인 m+4를 사용하여 도함수를 경계 지어야 하지만, 해당 Lean 정리는 대신 5개의 추가 차수인 m+5를 필요로 합니다. 이는 논문이 명시한 것보다 더 강한 조건입니다. 다른 경우, 원고의 방정식 10.19는 B_R이라고 불리는 하나의 변수만 사용하여 압력 플럭스 항을 경계 지으나, 동일한 경계의 Lean 버전도 다른 수학 기법에서 파생된 두 번째 변수인 A_R에 의존합니다.

저자들은 Lean 파일이 성공적으로 컴파일되는 것은 명시된 정리에 대해 어떤 올바른 증명이 존재함을 보여줄 뿐이며, 단어로 설명한 것과 동일한 증명임을 보여주지 않는다고 결론 내립니다. OpenAI의 Lean 코드는 자연 언어 논문의 해당 결과보다 다양한 함수의 경계에 종종 더 강한 조건을 적용한다고 말합니다. OpenAI의 Navier-Stokes 및 관련 Euler 방정식 형식화가 신뢰되기 전에 전통적인 증명이 받는 것과 동일한 동료 검토를 받을 것을 권장합니다.

별도의 논쟁: 어느 문제가 해결되었는가?

번역 문제와는 별개로, 여러 수학자들은 OpenAI가 대부분의 연구자들이 관심을 갖는 Navier-Stokes 버전을 해결했는지 여부에 대해 이의를 제기했습니다. Clay Institute의 2000년 공식 문제 진술은 Charles Fefferman에 의해 작성되었으며, 부드러운 외부 강제항을 허용하는 옵션 C를 포함하지만, 대부분의 수학자들은 강제되지 않은 경우에 초점을 맞춰왔습니다. Scientific American이 보도했습니다.

OpenAI의 증명은 옵션 C를 목표로 합니다. 시카고 대학의 Luis Silvestre와 동료들은 외부 력이 제거되면 OpenAI의 블로우업 메커니즘이 작동할 수 없다고 주장하는 논문을 게시했습니다. Scientific American이 보도했습니다.

광범위한 정밀 조사 패턴의 일부

OpenAI의 수학적 주장에 대한 정밀 조사는 새로운 것이 아닙니다. 2025년 10월, 당시 OpenAI 부사장 Kevin Weil은 GPT-5가 이전에 해결되지 않은 10개의 Erdős 문제를 해결했으며 11개 이상의 문제에서 진전을 이루었다고 말했습니다. Thomas Bloom을 포함한 수학자들은 결과가 이미 발표된 문헌에 존재한다고 말했으며, Weil은 게시물을 철회했습니다. TechCrunch가 보도했습니다. OpenAI가 2026년 5월 추론 모델이 1946년으로 거슬러 올라가는 Erdős 기하학적 추측을 반박했다고 발표했을 때, 수학자 Noga Alon, Melanie Wood, Thomas Bloom의 지지 진술을 발표했습니다. Thomas Bloom은 이전의 오류를 지적한 동일 인물입니다. TechCrunch가 보도했습니다.

2026년 10월 7일, OpenAI는 GitHub에 372개의 AI 생성 수학 결과를 발표했습니다. 각각은 열린 문제를 해결하거나 그에 대한 실질적인 진전을 이루기 위해 의도되었으며, 대부분은 내부 모델에 대한 단일 프롬프트에서 생성되었으며, 각각 약 3시간의 ChatGPT Pro 컴퓨팅 시간의 비용이 들었습니다. the-decoder가 보도했습니다. 25명의 Fields Medal 수상자들은 진정한 수학적 진술을 대량 생산하면 해당 분야를 진전시키지 않고 해치는 위험이 있다는 공개 서한에 서명했습니다. 동일 보도에 따르면 대부분의 결과는 표준적인 동료 검토를 거치지 않았습니다.

주장이 현재 어디에 서 있는가

Clay Mathematics Institute는 여전히 Navier-Stokes를 미레니엄 상 문제 중 하나로 미해결로 나열합니다. implicator.ai가 보도했습니다. Institute 회장 Martin Bridson은 발표가 흥미로웠지만 어떤 공식적인 평가도 서두르지 않고 엄격하게 진행될 것이라고 말했습니다.