논문 제출: 2026년 10월 6일. 비판 대상 최초 발표: 9월 8일.

Alexander Bastounis, Fabian Circelli, Anders C. Hansen이 10월 6일 제출한 프리프린트는 OpenAI의 나비에–스토크스 증명에서 자연어 설명과 Lean 형식화가 일치하지 않는다고 주장한다. 핵심은 Lean이 확인한 논리와 사람이 읽는 논증의 대응 관계다.

1. 저자들이 제시한 두 사례

첫째, 자연어 논문의 미분 추정은 m+4차 미분을 사용하는데 대응 Lean 결과에는 m+5차가 필요하다는 지적이다. 둘째, 압력 플럭스 추정에서는 자연어 표현과 Lean의 경계식 및 증명 방법이 다르며, Lean 쪽에는 추가량 A_R이 들어간다고 설명한다. 분석은 저장소의 특정 커밋 f9e8bc5를 대상으로 한다.

저자들은 또한 모든 수학적 문장의 모호성을 일반적으로 해결하는 문제에 계산 가능성의 근본적 한계가 있다고 논증한다. 이를 개별 형식화 작업이 모두 불가능하다는 결론으로 확대해서는 안 된다. 비판 논문 원문, 3·4절

2. 이 비판이 아직 확정하지 않은 것

이 글은 저자들의 프리프린트 비판을 전하는 것이며, 최종 정리의 오류를 독립적으로 확인했다는 보도가 아니다. 원문과 다른 논증이 형식화됐다는 지적만으로 최종 정리가 거짓이 되지는 않는다. 확인할 대상은 최종 명제·가정의 적절성, 형식 증명의 타당성, 자연어 설명과의 대응이다.

OpenAI는 9월 8일 내부 시스템이 증명과 Lean 형식화를 만들었다고 발표했다. 회사 설명상 나비에–스토크스 작업에는 약 1만 동시 에이전트, 출력 토큰 약 1,300억 개가 사용됐으며, 해법 도출 뒤 형식화·검증에 17시간이 추가됐다. 이는 이번 비판 연구의 실험 예산이 아니다. OpenAI 최초 발표