Lean이 확인한 것은 다른 명제였다: OpenAI 나비에-스토크스 증명의 형식화를 짚은 논문

컴파일러가 통과시킨 코드도 요구사항과 다른 일을 할 수 있습니다. 수학의 증명 검사기도 마찬가지입니다. 영국 케임브리지대와 킹스칼리지런던 소속 수학자 세 명이 10월 6일 arXiv에 논문을 올렸습니다. OpenAI가 Lean으로 검증했다고 밝힌 나비에-스토크스 방정식 증명이 실제로는 원래 논문과 다른 명제를 증명한다는 지적입니다.

먼저 무엇을 검사했는지부터 살펴보겠습니다. OpenAI는 나비에-스토크스 방정식의 해가 유한한 시간 안에 폭발한다는 증명을 자연어 논문으로 내고, 그 내용을 Lean 4로 옮긴 코드도 GitHub에 함께 올렸습니다. Lean은 증명의 논리를 컴퓨터가 한 단계씩 확인하는 프로그래밍 언어입니다. 자연어 증명을 Lean으로 옮기는 일을 자동 형식화라고 부릅니다. 이번에는 이 번역도 AI가 맡았습니다.

논문 저자들은 번역이 원문과 어긋나는 지점을 여러 곳에서 찾았습니다. 자연어 논문의 보조정리 8.6은 어떤 함수의 m번 미분을 입력의 m+4번 미분으로 묶을 수 있다고 주장합니다. 하지만 이 보조정리에 대응하는 Lean 코드가 증명한 것은 m+5번 미분이 필요한, 더 약한 명제였습니다. Lean은 그 약한 명제만 맞다고 확인했을 뿐, 논문이 실제로 주장한 더 강한 명제는 검사하지 않았습니다.

저자들은 OpenAI의 자연어 증명이 틀렸다고 주장하지는 않았습니다. 다만 Lean 코드가 컴파일됐다는 사실만으로는 자연어 증명이 맞다고 말할 수 없으므로, 다른 증명처럼 동료 검토를 거쳐야 한다고 결론지었습니다. 고등연구소(IAS)의 수학과 AI 자문단도 9월 말에 낸 권고문에서 자연어 증명과 형식 증명의 대응 관계를 기계가 읽을 수 있는 메타데이터로 함께 내면 도움이 된다고 밝혔습니다. TechCrunch는 OpenAI가 이번 공개에서 그 메타데이터를 붙이지 않았다고 전했습니다.

이제 개발자가 따져 볼 질문도 달라집니다. 지금까지는 AI가 만든 결과에 검사가 붙었는지가 중요했습니다. 하지만 검사할 명제까지 AI가 직접 옮기면, 검사를 통과했다는 사실은 AI가 옮긴 명제가 맞다는 뜻일 뿐입니다. 코딩 에이전트가 코드와 테스트를 함께 쓰고, 그 테스트는 원래 요구사항보다 느슨한 조건만 확인하는 상황과 같습니다.

그래서 사람이 읽어야 할 자리도 바뀝니다. 수천 줄에 이르는 증명이나 구현을 전부 읽을 수는 없어도, 검사 대상을 밝힌 명제와 테스트의 단언문은 짧습니다. 요구사항 한 줄마다 이를 확인하는 검사가 어디에 있는지 대응표를 만들어 두면, 검사가 통과했다는 보고를 받았을 때 무엇이 통과했는지 바로 확인할 수 있습니다.

결국 검증 도구가 강해질수록 사람이 맡아야 할 일은 결과 전체를 살피는 것이 아니라 검사의 대상을 확인하는 것입니다. AI에게 코드와 테스트를 함께 맡긴다면, 이번 주에는 테스트가 확인하는 조건을 요구사항 문서와 한 줄씩 대조해 보시기 바랍니다.

출처

1. arXiv: Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs, 2026년 10월 6일 게시. Alexander Bastounis, Fabian Circelli, Anders C. Hansen 작성. 보조정리 8.6의 m+4번과 m+5번 미분 비교는 논문 예시 3.1입니다.
2. OpenAI: openai/NavierStokesAndEuler 저장소, 2026년 9월 공개. 나비에-스토크스와 오일러 방정식 결과의 Lean 4 형식화입니다.
3. 고등연구소 수학과 AI 자문단(AGMAI): Responsible Release of AI-Generated Mathematics, 2026년 9월.
4. TechCrunch: OpenAI's math solutions aren't meeting the field's standards yet, 2026년 10월 8일.