인공지능이 코드 생성에서 더 나아가 인류가 수십 년 동안 풀지 못한 수학 난제에 손을 대기 시작했다. 오픈AI가 오랜 미해결 과제였던 나비에-스토크스 방정식의 해법을 내놓은 것이다. 수만 개 단위의 AI 에이전트가 협업하고 그 결과를 정형 검증 언어로 확인하는 방법론을 실제로 보여줬다는 점에서 개발자에게도 시사하는 바가 크다.

오픈AI, 나비에-스토크스 난제 해법 발표

오픈AI는 2026년 9월 8일 공식 블로그에서 클레이수학연구소 7대 밀레니엄 난제 중 하나인 나비에-스토크스 존재성과 매끄러움 문제의 해법을 발표했다. 유체역학에서 약 90년 동안 풀리지 않던 이 문제에 오픈AI는 대규모 컴퓨팅 자원을 쏟아부었다.

작업에는 최근 출시된 GPT-6 Astra가 아니라 공개되지 않은 차세대 내부 모델이 쓰였다. 이 미공개 모델로 돌아가는 1만 개의 AI 에이전트가 동시에 협력하며 증명을 이끌었고, 이 과정에서 출력 토큰 약 1300억 개가 소비됐다.

오픈AI는 유한 시간 안에 유체의 회전 속도 등이 무한대로 치솟아 물리 법칙이 무너지는 반례를 찾아 문제를 풀었다고 주장했다. 이를 증명하는 165쪽 분량의 논문 원고와 함께, 컴퓨터 증명 보조 언어인 린 형식의 정형 검증 코드를 깃허브 등에 공개했다.

오픈AI가 1만 개의 에이전트를 동원해 90년 미해결 난제인 나비에-스토크스 방정식의 해법을 제시했다.

88시간의 협업과 정형 검증

증명이 완성되기까지 AI 에이전트들은 촘촘하게 협업했다. 1만 개의 에이전트가 서로 270만 개의 메시지를 주고받았고, 이 소통과 추론을 마치는 데 총 88시간이 걸렸다. 인간 수학자라면 수년, 어쩌면 평생이 걸렸을 작업이 사흘 만에 끝난 셈이다.

논리의 빈틈을 없애기 위한 정형화와 검증에는 17시간이 더 들었다. AI가 만든 증명에 논리 오류가 없는지 컴퓨터가 읽을 수 있는 언어로 다시 확인하는 작업이었다.

역할 분담도 흥미롭다. 증명을 설계하고 해법을 찾는 단계에는 비공개 차세대 내부 모델이 쓰였지만, 린 정형화와 검증은 최근 출시된 GPT-6 Astra가 맡아 검증을 마쳤다.

AI 에이전트들은 88시간 동안 메시지를 주고받으며 해법을 찾았고 17시간 동안 Lean 검증을 수행했다.

상금 포기와 우선권 논란

오픈AI는 발표와 함께 클레이수학연구소가 내건 100만 달러 상금을 받지 않겠다고 밝혔다. 상금보다는 AI 발전 속도를 세계에 보여주고 앞으로 나올 자사 모델에 대한 기대를 투명하게 공유하는 편이 더 가치 있다는 것이 오픈AI가 밝힌 이유다.

발표 뒤에는 학계와의 갈등과 저작권 논란이 따라붙었다. 발표 직전 앤트로픽 소속 연구원과 뉴욕대 교수가 함께 낸 오일러 방정식 관련 성과가 오픈AI 프롬프트에 미리 흘러 들어가 도용됐다는 의혹이 나왔다.

수학계 일부에서는 오픈AI가 외부의 핵심 연구 성과를 사전 유출 경로로 손에 넣어 자사 모델에 학습이나 프롬프트 형태로 넣고 지름길을 택했다고 비판했다. AI 난제 해결이라는 성과에 학술적 우선권과 연구 윤리 문제가 얽혀 있는 셈이다.

오픈AI는 100만 달러 상금 수령을 포기했으나 사전 유출 및 성과 가로채기 논란에 휩싸였다.

검증 과제와 미공개 정보

오픈AI가 주장한 성과가 학계의 공식 인정을 받으려면 아직 거쳐야 할 단계가 많다. 먼저 이번 작업에서 결정적 역할을 한 비공개 내부 모델에 대해 오픈AI는 코드명이나 파라미터 크기 같은 세부 스펙을 하나도 공개하지 않았다.

공식 검증 절차도 멀었다. 클레이수학연구소 기준으로 밀레니엄 난제 해결이 최종 확정되려면 최소 2년간의 학계 동료평가를 통과해야 한다.

그 사이 증명 내용은 계속 고쳐지고 있다. 발표 당일 처음 공개된 원고는 165쪽이었는데, 이후 참고문헌과 역사적 배경에 대한 사사 표기 등이 보완되면서 공식 논문은 166쪽으로 늘었다.

내부 모델의 세부 스펙은 베일에 싸여 있으며 수학계의 공식적인 동료평가 절차가 남아있다.

개발자가 주목해야 할 AI 수학의 미래

이번 일은 수학계 소식이면서 개발자가 AI를 쓰는 방식이 바뀌고 있다는 신호이기도 하다. AI는 사람이 시키는 대로 코드 한 덩어리를 짜는 보조 도구에서, 만 개 단위의 에이전트가 협업해 가설을 세우고 스스로 검증하는 해결사 쪽으로 옮겨 가고 있다.

특히 수학적 엄밀함을 보증하는 정형 검증 언어 린과 생성형 에이전트 모델의 조합은 높은 무결성이 필요한 소프트웨어 아키텍처 설계나 우주·금융 같은 미션 크리티컬 시스템 개발에 그대로 가져다 쓸 수 있는 패턴이다.

상용 모델보다 앞선 능력을 보여주는 프론티어 모델의 움직임은 개발 환경에도 큰 영향을 줄 것으로 보인다. 개발자들은 AI가 내놓은 결과의 논리적 엄밀성을 자동으로 확인하는 정형 검증 체계와 에이전트 오케스트레이션에 관심을 두고 대비할 필요가 있다.

참고