OpenAI, AI 시스템이 Lean으로 형식화된 나비에–스토크스 반증을 생성했다고 주장
OpenAI는 내부 AI 시스템이 나비에–스토크스 방정식에서 유한시간 특이점을 발견했다고 말하지만, 독립적인 수학자 검토는 여전히 필수적이다.
OpenAI는 내부 AI 시스템이 3차원 비압축성 유체 운동이 유한 시간 특이점을 일으킬 수 있음을 보이는 분석적 증명을 만들어, 나비에–스토크스 존재성과 매끄러움 문제를 다뤘다고 말한다. 회사는 서면 논증과 Lean 형식화를 공개했지만, उपलब्ध한 증거만으로는 이 주장이 독립적으로 검증되지 않았다.
이 발표가 중요한 이유는 나비에–스토크스 문제가 2000년 Clay Mathematics Institute가 지정한 7대 밀레니엄 문제 중 하나이기 때문이다. 올바른 해법은 자동화된 수학 연구의 한계뿐 아니라, 수십 년 동안 인간 연구자들을 좌절시켜 온 문제에 AI 시스템을 어떻게 시험할 것인가에도 영향을 미칠 것이다.
OpenAI의 글이 이 보도의 주요 출처다. 함께 제공된 와이어 기사에는 이용 가능한 자료상 추가 기사 본문이 없으므로, 시스템의 성능, 규모, 결과에 대한 가장 강한 주장은 공급업체 보고에 의존한다.
OpenAI가 해결했다고 말하는 것
OpenAI는 자사 시스템이, 처음에는 정지해 있던 매끄러운 유체가 매끄러운 외력에 놓인 채 유한 에너지를 유지하면서 유한 시간 안에 특이점을 형성하는 문제 설정을 확립했다고 말한다. 회사의 설명에 따르면, 이 결과는 나비에–스토크스 문제의 공식 서술에서 “C”와 “D” 명제를 증명하는 것으로, 모든 해가 정칙하게 남는다는 증명이라기보다 보편적 매끄러움의 반증에 해당한다.
제안된 메커니즘은 안쪽으로 나선형을 그리며 축을 따라 늘어나는 소용돌이다. 중심 영역이 수축함에 따라, 유체의 속도는 수학적 모델에서 한계 없이 증가한다. OpenAI는 이 구성이 가속도, 압력, 운동량 전달, 점성 항이 커지면서도 정밀한 방식으로 서로 상쇄되는 데 의존한다고 말한다. 외력은 매끄러운 상태를 유지하므로, 주장된 붕괴는 무한한 힘을 직접 주입한 것이 아니라 유체역학 자체에 의해 발생한다.
나비에–스토크스 방정식은 뉴턴의 운동 법칙을 사용해 유체를 연속체로 모델링한다. 엔지니어와 과학자들은 항공기 설계, 일기 예보, 혈류 분석 등에 이를 사용한다. 아직 풀리지 않은 질문은 일정한 밀도를 가진 매끄러운 3차원 비압축성 흐름이 모든 시간 동안 매끄러워야 하는가이다.
대규모 다중 에이전트 실험
OpenAI에 따르면, 작업은 회사가 두 개의 밀레니엄 문제가 해결됐다는 소문을 들은 9월 1일에 시작됐다. 이후 오케스트레이션 시스템이 AI 에이전트들에게 모든 열린 문제와 몇 가지 관련 질문을 검토하도록 지시했다.
회사는 나비에–스토크스 작업에 약 1만 개의 동시 에이전트가 참여했다고 말한다. 이 에이전트들은 그룹으로 나뉘었고, 서로 다른 문제 정식을 받았으며, 캐시된 인터넷 버전과 코드 실행을 포함한 도구를 사용할 수 있었다. OpenAI는 가장 유망한 작업을 통합하기 전에, 증명과 반증 변형 모두를 탐색했다고 말한다.
OpenAI는 더 넓은 프로젝트가 490만 개의 메시지를 생성했고 약 3000억 개의 출력 토큰을 사용했다고도 보고한다. 나비에–스토크스 작업에 한정하면, 270만 개의 메시지와 약 1300억 개의 출력 토큰을 사용했다고 한다. 이 수치는 회사의 내부 실험을 설명할 뿐이며, 유용한 수학적 추론에 대한 독립 감사 측정치는 아니다.
회사에 따르면 에이전트들은 약 88시간의 작업 끝에 9월 5일 나비에–스토크스 결과에 도달했다. OpenAI에 따르면 Lean 형식화와 검증에는 GPT-6 Astra를 통해 추가로 17시간이 걸렸다. 회사는 검색 과정에서 서로 다른 에이전트 그룹의 통찰을 통합하기 위해 Codex를 사용했다고 말한다.
형식 검증은 증거이지 최종 승인 아님
Lean 산출물은 형식화가 전통적인 연구 초안에서는 살아남을 수 있는 누락된 가정과 잘못된 단계를 드러낼 수 있기 때문에 OpenAI 공개의 중요한 부분이다. 하지만 그것만으로는 형식화된 진술이 공식 밀레니엄 문제 정식화와 정확히 일치하는지, 또는 구현에 정의, 가져온 보조정리, 가설의 오류가 있는지는 결정할 수 없다.
OpenAI는 증명 초안과 Lean 형식화를 공개했지만, 제공된 증거에는 Clay Mathematics Institute나 독립 수학자들의 검토가 포함되어 있지 않다. 회사는 이 결과로 밀레니엄 상을 주장할 의도가 없다고 명시한다. 이 구분은 중요하다. 공개된 AI 생성 증명은 연구 주장인 반면, 상의 인정은 전문가의 심사와 연구소 규칙에 따른 수용이 필요하다.
시점 역시 신중한 귀속을 요구한다. OpenAI는 Anthropic 직원인 Levent Alpöge와 뉴욕대학교 수학 교수 Tristan Buckmaster와 관련된 소문을 들은 뒤 작업을 시작했다고 말한다. 회사는 그들의 작업이 같은 나비에–스토크스 결과가 아니라 강제 Euler에 관한 것이었고, 두 작업은 방법과 정확한 결론 모두에서 달랐다고 말한다. OpenAI는 공개 이전에 그들의 특정 사용자 데이터나 작업에 접근하지 않았다고 말하지만, 비식별화된 제품 데이터가 자사 모델 개선에 도움이 되었을 가능성은 배제할 수 없다고 인정한다.
이 결과가 AI 빌더에게 의미할 수 있는 것
AI 개발자에게 중요한 변화는 단순히 모델이 수학 텍스트를 생성했다는 사실이 아니다. OpenAI는 많은 에이전트가 독립적으로 정식을 탐색하고, 중간 결과를 교환하며, 소프트웨어 도구를 사용하고, 후보 증명을 형식 검증 시스템에 넘기는 워크플로를 설명한다. 이 구조는 단일 챗봇 응답이라기보다 자동화된 연구 파이프라인에 가깝다.
이 접근은 비용과 운영 위험도 드러낸다. 수천억 개의 생성 토큰과 수천 개의 동시 에이전트는 고가치 연구 벤치마크에는 실용적일 수 있지만, 일반 소프트웨어 제품의 경제성과는 거리가 멀다. 빌더들은 병렬 탐색이 진정 새로운 통찰을 만들어내는지, 아니면 그럴듯하지만 중복된 추론의 양만 늘리는지 측정해야 한다.
기업 구매자에게 이 사건은 모델이 결과를 제안할 수 있는 능력과 조직이 그것을 신뢰할 수 있는 능력의 차이를 다시 강조한다. 과학 및 엔지니어링 워크플로에서는 재현 가능한 산출물, 기계 검증 가능한 증명, 전문가 검토, 명확한 가정 기록이 벤치마크 점수나 에이전트 실행 규모보다 더 중요하다. Lean 형식화는 그 과정을 지원할 수 있지만, 도메인 전문성의 필요성을 없애지는 못한다.
이 발표는 경쟁 신호이기도 하다. OpenAI는 내부 모델이 GPT-6 Astra보다 더 뛰어나며 학습은 여전히 진행 중이라고 말한다. 이러한 역량 비교는 OpenAI의 주장에 근거하므로, 확정된 시장 측정치가 아니라 내부 또는 공급업체 보고 주장으로 다뤄야 한다.
다음에 주목할 점
첫 번째 신호는 공개된 증명과 Lean 코드에 대한 독립 검토이며, 특히 그 구성이 공식 나비에–스토크스 서술의 모든 조건을 충족하는지 여부다. 미묘하게 다른 정의역, 외력 조건, 또는 특이점 개념에 의존하는 형식 증명은 같은 문제를 해결하지 못한다.
두 번째는 수학자들이 결과를 재현하고, 빈틈을 찾아내거나 형식화가 컴파일되고 논증을 충실히 인코딩하는지 확인하는지다. Clay Mathematics Institute의 반응도 이 작업이 인정 기준을 충족하는지 명확히 해줄 것이다.
연구자들은 또한 OpenAI가 모델 버전, 프롬프트, 도구 경계, 계산 자원 회계를 포함해 다중 에이전트 탐색을 재현할 수 있을 만큼의 구현 세부 정보를 공개하는지 지켜봐야 한다. 그런 정보가 없으면 보고된 에이전트 수와 토큰 총계는 맥락을 제공하지만, 유사한 시스템을 구축하는 팀에는 제한적인 지침만 준다.
Creati.ai 관점
OpenAI의 발표는 아직 확정된 수학적 사실이 아니라 중요한 역량 주장으로 이해하는 것이 가장 좋다. 에이전트 조정, 코드 도구, Lean 형식화의 결합은 AI 지원 연구를 위한 설득력 있는 방향이지만, 핵심 결과는 여전히 이를 만든 회사 밖의 검토에 달려 있다.
빌더에게 실용적인 교훈은 헤드라인보다 더 좁고 더 유용하다. 고급 AI 연구 시스템에는 검증 계층, 명시적 문제 명세, 독립 검토가 필요하다. 이 결과를 둘러싸고 그러한 통제가 견디는지 확인된다면, 이 사건은 기계 보조 수학의 의미 있는 사례 연구가 될 수 있다. 그렇지 않다면, 유창한 증명과 형식적으로 보이는 산출물이 수학적 검증을 대체할 수 없는 이유를 보여주게 될 것이다.
