OpenAI 나비에-스토크스 AI 수학 증명, 자연어 논문과 Lean 검증 간 중대 불일치 발견

OpenAI가 공개한 나비에-스토크스(Navier–Stokes) 방정식 해법 논문의 자연어 서술과 Lean 대화형 정리 증명기(Interactive Theorem Prover) 검증 코드 사이에 중대한 불일치가 존재한다는 학술 분석(arXiv:2610.08144)이 2026년 10월 8일 공개되었습니다.

이미지 출처: X @ValerioCapraro / arXiv:2610.08144

이번 분석은 AI가 생성한 자연어 수학 논증을 기계 검증 가능한 형식 언어로 변환할 때, AI가 가정을 임의로 바꾸거나 원래 증명하고자 했던 정리 자체를 환각할 수 있다는 '형식 검증 정렬(alignment) 문제'를 구체적으로 드러냈습니다.

자연어 논문과 Lean 검증 코드 간 핵심 불일치 2가지

공개된 분석 논문에 따르면, OpenAI의 나비에-스토크스 관련 논문에서 자연어로 기술된 증명과 실제 Lean 코드로 작성되어 기계 검증을 통과한 명제 사이에 최소 2건 이상의 구조적 차이가 확인되었습니다.

• 입력 도함수(Input Derivatives) 요구 조건 차이: 자연어 논문 본문에서는 4개의 추가 입력 도함수만으로 충분하다고 기술했으나, 실제 Lean 형식 검증 코드에서는 5개의 도함수를 요구하도록 작성되었습니다. 이는 수학적으로 원래 목표했던 명제보다 조건이 더 까다로운 약화된 결과(weaker result)를 증명한 셈이 됩니다.
• 압력-플럭스(Pressure-Flux) 추정 경로의 상이성: 압력-플럭스 추정치 유도 과정에서도 자연어 설명에서 제시된 경계(bound) 및 증명 논리와 전혀 다른 경로와 경계를 사용하여 Lean 코드가 구성되었습니다.

이로 인해 Lean 검증기 자체는 오류 없이 통과했음에도 불구하고, 검증된 수학적 대상이 자연어 논문이 주장하던 본래 정리와 일치하지 않는 간극이 발생했습니다.

Lean 검증 통과와 '다른 정리의 환각' 리스크

이번 사례는 AI 기반 수학 연구에서 기계적 형식 검증(Lean)이 갖는 맹점을 시사합니다.

컴퓨터 검증기인 Lean은 입력된 형식 코드의 논리적 무결성만을 검증할 뿐, 그 코드가 연구자가 원래 자연어로 의도했던 정리와 동일한 대상을 가리키고 있는지는 판단하지 못합니다. AI가 자연어 논증을 Lean 코드로 번역·형식화하는 단계에서 가정을 은근히 변경하거나 명제를 약화시킬 경우, 기계는 '올바른 증명'으로 승인하지만 실제로는 엉뚱한 정리를 증명하는 '환각된 정리(hallucinated theorem)'가 만들어질 수 있습니다.

현재 학계 평가와 남겨진 과제

학계에서는 이번에 지적된 불일치들이 OpenAI의 나비에-스토크스 증명 전체를 완전히 무효화(invalidate)하는지 여부에 대해 면밀한 추가 검토를 진행하고 있습니다.

현재 단계에서는 증명의 전면 파기 여부보다는, 수백 편 단위로 쏟아지는 AI 생성 수학 논문에서 자연어 주장과 형식 검증 명제 사이의 의미적 일치성을 검증하는 독립적인 평가 체계가 필수적이라는 점에 논의가 집중되고 있습니다.

출처

• arXiv:2610.08144 연구 논문
• X @ValerioCapraro 분석 원문