오픈AI가 9월 8일 「나비에-스토크스 밀레니엄 문제에 대하여」를 올리며 서술 원고와 린 형식 증명을 함께 공개했고, 165쪽 논문의 정리 1.1 은 점성이 양수인 모든 경우에 대해 시간과 공간에서 유한한 범위에만 작용하는 매끄러운 외력을 하나 잡아, 정지 상태에서 출발한 속도가 유한 시간에 무한대로 가면서도 운동 에너지는 유한하게 유지되는 해를 구성해요. 논문은 이것이 찰스 페퍼먼이 쓴 공식 문제 진술의 (C) 와 (D) 를 세운다고 적었는데, 그 진술에서 (A)·(B) 는 외력을 0 으로 고정하고 (C)·(D) 만 매끄러운 외력을 허용하며 넷 중 하나만 증명하면 된다고 되어 있어요. 같은 접근법으로 연구하던 뉴욕대 트리스탄 버크마스터는 공개 성명에서 오픈AI 쪽으로부터 '사람 손은 거의 안 들어갔다'고 들었지만 통화 도중 사실이 아닌 것으로 드러났고 자기들의 코덱스 세션이 학습에 쓰였는지 물었을 때는 답을 받지 못했다고 적었는데, 오픈AI 연구 총괄 마크 첸은 기자들에게 사람도 AI도 문제를 풀려고 사용자 데이터를 찾아보지 않았다고 답했어요.
용어 풀이
- 린 (Lean)
- 증명의 논리 단계를 하나씩 기계가 검사해 주는 정리 증명 도구
- 형식 증명
- 사람이 읽고 판단하는 대신 기계가 검사할 수 있게 적은 증명
- 코덱스 (Codex)
- 오픈AI가 만든 코딩 에이전트
운영자 인사이트
린은 증명이 논리적으로 맞는지를 기계로 확인해 주지만, 무엇을 증명 대상으로 삼았는지와 그 착상이 어디서 왔는지는 확인해 주지 않아요. 에이전트가 낸 산출물을 받을 때도 검사 통과 여부와 별개로 명제의 범위와 입력 출처를 따로 확인하는 절차를 두세요.
여러 관점으로 보기
- 클레이 공식 문제 진술 페퍼먼이 쓴 공식 진술은 (A)·(B) 에서 외력을 0 으로 고정하고 (C)·(D) 에서만 매끄러운 외력을 허용하며, 네 항 중 하나만 증명하면 된다고 적어 뒀어요. Clay Mathematics Institute
- 같은 접근법으로 연구하던 수학자의 성명 버크마스터는 오픈AI 증명을 본 적이 없고 아무도 고발하지 않는다면서도, 사람 손이 거의 안 들어갔다는 설명이 통화 중에 뒤집혔고 학습 데이터 질문에는 답을 못 받았다고 적었어요. Tristan Buckmaster (NYU Courant)
- 오픈AI 쪽 해명 오픈AI는 9월 1일부터 에이전트 1만 개를 88시간 돌렸고 비용은 수백만 달러대라고 밝혔으며, 상금 100만 달러는 청구하지 않겠다고 했어요. The Next Web
- 수학계 반응 문제 진술을 쓴 찰스 페퍼먼은 '문제가 풀려서 기뻤다'면서 이야기의 주역은 이 접근법을 연 코르도바와 마르티네스소로아라고 했어요. Quanta Magazine
- 저자 표기 분쟁 오픈AI 세바스티앙 뷔벡은 공동 저자 이름을 빼 달라고 요구했다는 주장을 부인했어요. Engadget
- 개발자 토론 해커뉴스에서 오픈AI 발표가 1,062점에 댓글 907개, 버크마스터 성명이 1,169점에 댓글 515개를 모았고, 증명이 맞느냐보다 어느 항을 세웠느냐와 학습 데이터 질문에 답이 없다는 점이 반복해서 지적됐어요. Hacker News