번역 과정에서 의미를 잃은 Navier-Stokes

Lean 검증 통과는 생성된 형식 증명의 타당성을 확인하지만, 그 증명이 원래 자연어 논증을 충실하게 옮겼거나 자연어 증명 자체가 올바르다는 보장은 아님

자동 형식화에는 이미 정확히 형식화된 정리의 증명을 생성하는 작업과, 정의부터 증명까지 수학적 의미를 보존해 번역하는 작업이 있으며, 두 작업의 성공 기준은 다름

간단한 다항식과 대칭행렬 사례에서 AI는 잘못된 자연어 증명을 고치거나 올바른 논증을 다른 논증으로 대체해 컴파일되는 Lean 증명을 생성함

OpenAI가 발표한 Navier-Stokes 폭발 증명의 자연어 문서와 Lean 코드 비교에서는 추가 미분 차수, 압력 플럭스 추정식, 증명 방법이 서로 일치하지 않는 사례가 확인됨

자연어 증명의 정확성에는 통상적인 동료 심사와 검토가 여전히 필요함. 이 연구는 OpenAI 자연어 증명의 정오를 판정하지 않으며, Lean 번역의 의미 불일치만을 검토함

자동 형식화의 두 가지 성공 기준

첫 번째 유형은 정리의 명제가 이미 Lean으로 정확히 번역됐다는 전제에서, 자연어 증명을 입력받아 해당 정리의 형식 증명을 생성하는 작업임

sorry나 추가 공리 없이 Lean이 유효한 증명으로 받아들이고 컴파일하면 성공으로 간주함

이 기준은 원래 자연어 논증을 그대로 보존했는지까지 요구하지 않음

두 번째 유형은 수학 문서 전체를 의미에 충실하게 번역하는 작업임

정의, 정리, 명제, 증명뿐 아니라 개념과 결과 사이의 의존 관계도 보존해야 함

원문의 증명 검증이 목적이라면 형식 증명과 실제로 쓰인 논증 사이의 대응도 확립해야 함

다른 명제로 바꿔 증명하는 것은 원문의 의미를 보존한 번역이 아님

형식 증명의 정확성과 원문에 대한 충실성은 별개임

잘못된 자연어 증명을 올바른 형식 증명으로 바꿀 수 있음

두 증명이 모두 올바르지만 서로 다른 논증일 수 있음

자연어 문서가 형식 증명보다 강한 결과를 담고 있을 수도 있음

의미에 충실한 번역은 첫 번째 유형보다 훨씬 어려우며, 일반적인 경우 정지 문제보다 엄밀히 더 어려운 문제임

Lean은 형식화된 정리의 정확성을 확인할 뿐, 자연어 증명의 중간 논증과 보조정리까지 자동으로 검증하지 않으므로 동료 심사와 통상적인 검토를 생략할 근거가 되지 않음

기본 사례: 증명이 바뀌어도 Lean 검증은 통과함

예제 2.1은 (p(x)=x^3-x^2-x+1)이 (x\geq-1)에서 음이 아니라는 올바른 명제에 잘못된 자연어 증명을 붙인 사례임

자연어 증명은 근 (-1)의 중복도를 2, 근 (1)의 중복도를 1로 잘못 적고, (p(x)=(x-1)(x+1)^2)라는 잘못된 인수분해를 사용함

해당 구간에서 두 인수가 모두 음이 아니라는 설명도 잘못됐으며, 근에서 인수분해를 도출하는 과정에는 최고차항 계수에 대한 확인도 빠져 있음

ChatGPT-6 (Astra Ultra) 는 이 논증을 Lean으로 옮겨 달라는 요청에 근의 중복도를 바로잡은, 컴파일되는 올바른 증명을 반환함

따라서 생성된 Lean 증명의 성공은 입력된 자연어 증명의 정확성을 입증하지 않음

예제 2.2는 실수 대칭행렬 (A)에 대해 (\operatorname{tr}(A^2)\geq0)임을 보이는 두 가지 올바른 증명을 비교함

자연어 증명은 정규직교 고유기저로 대각화하고, 기저 변경에 대한 대각합의 불변성을 이용해 (\sum_i\lambda_i^2\geq0)을 얻음

AI가 생성한 Lean 증명은 대각화하지 않고 원래 행렬에서 (\operatorname{tr}(A^2)=\sum_{i,j}a_{ij}a_{ji})를 계산한 뒤, 대칭성을 이용해 (\sum_{i,j}a_{ij}^2\geq0)을 얻음

두 증명은 모두 맞지만, 대각화 논증을 생략하고 대칭성으로 대체했으므로 원래 논증의 충실한 번역은 아님

Navier-Stokes 비교의 대상과 범위

3차원 비압축성 Navier-Stokes 정칙성 문제는 1934년 Leray의 기초 연구로 거슬러 올라가며, 2000년 Clay 밀레니엄 문제로 지정됨

OpenAI의 발표에 동반된 openai/NavierStokesAndEuler 저장소는 자연어 문서인 “Finite time blowup for Navier–Stokes”와 “Finite time blowup for the Euler equation”의 결과를 Lean 4로 형식화했다고 명시함

비교 대상은 자연어 Navier-Stokes 문서와 커밋 f9e8bc5 의 관련 Lean 선언임

검토한 사례에서는 명제나 증명 방법이 달라, Lean 형식화만으로 자연어 증명의 정확성을 보장할 수 없음

이 비교는 OpenAI의 자연어 증명이 틀렸다고 판정하는 작업이 아니라, 번역의 의미적 충실성을 확인하는 작업임

역연산자 추정: 입력 미분 차수가 하나 더 필요함

보조정리 8.6의 식 (8.19) 와 대응하는 Lean 추정식은 같은 출력 미분 차수를 제어하는 데 필요한 입력 미분 차수가 다름

자연어 문서: (|N^{-1}F|{C_y^m}\leq C_m|F|{C_y^{m+4}})

Lean 추정: (|N^{-1}F|{C_y^m}\leq K_m|F|{C_y^{m+5}})

(m)은 음이 아닌 정수이며, Lean 쪽은 입력 미분을 하나 더 요구하므로 직접 비교 가능한 이 추정에서는 더 약한 결과임

여기서 (N^{-1}) 는 2차원 토러스 (\mathbb T^2=\mathbb R^2/\mathbb Z^2) 위의 미분 연산자 (N)에 대한 역연산자임

결론은 해당 미분 순서에 따른 (N^{-1}F)의 미분값을 같은 입력 상한 (C)의 상수배로 제어함

자연어 식과 직접 비교하려면 (|w|\leq m)인 모든 미분 순서에 대해 상한을 취해야 함

이 단계는 해당 Lean 정리 안에서 명시적으로 수행되지 않음

이를 수행하면 상수 (\widehat K_m=\max(K_0,\ldots,K_m))를 갖는 (C_y^{m+5}) 입력 노름 추정이 됨

미분 차수 불일치의 원인과 적용 범위

자연어 증명은 Fourier 급수의 감쇠율을 이용함

제수 추정 (|v_t\cdot k|^{-1}\leq C(1+|k|))에서 출발해, 출력보다 네 차수 높은 입력 미분으로 2차원에서 합산 가능한 ((1+|k|)^{-3}) 감쇠를 얻음

같은 논증으로 추정식, 매끄러움, 영 주파수 계수를 고정한 뒤의 유일성을 확보하며, 승수는 느린 계수 미분과 교환하고 실수값 성질을 보존함

Lean 증명은 coefficient_seminorm_bound 를 거쳐 ((1+|k_1|+|k_2|)^{-4}) 형태의 급수를 사용하므로, 입력 미분을 다섯 차수 더 요구함

inverse_finiteJets, mixedJet_inverse_bound에서도 (m+4)가 아닌 (m+5) 조건이 나타남

다만 inverse_finiteJets처럼 매개변수와 토러스의 혼합 미분을 사용하는 결과는 토러스 미분만 사용하는 자연어 식과 직접적인 강약 비교가 불가능할 수 있음

이 경우에도 추가 미분 차수가 다섯이라는 불일치는 남음

압력 플럭스: 추정식과 증명 방법이 함께 달라짐

식 (10.19) 는 속도 유일성을 보이는 보조정리 10.5의 중간 단계이며, 자연어 문서와 Lean은 다음처럼 서로 다른 상한을 얻음

자연어 문서는 거의 모든 (t\in(0,T))에 대해
[
\left|\int \pi w\cdot\nabla\chi_R\right|
\leq \frac{C_T}{R}
\left[(B_R+1)B_R^{1/2}+R^{-3/4}B_R^{3/4}\right]
]
을 사용함

Lean은 모든 (t\in(0,T))에 대해
[
\left|\int \pi w\cdot\nabla\chi_R\right|
\leq C_T\left[
(B_R^{1/2}+1)\left(\frac{A_R}{R}+\frac1{R^2}\right)
+R^{-7/4}B_R^{3/4}\right]
]
을 증명함

두 식 모두 (R\geq1)이며, 양변은 시간에 의존함. 유한한 비음수 상수 (C_T)는 (T)와 노름 규약에는 의존할 수 있지만 (R)에는 의존하지 않음

자연어 식 (10.17)은 (A_R)로 (B_R)의 상한을 주므로, 이를 역으로 사용해 Lean 식의 (A_R)를 제거할 수는 없음

따라서 두 상한을 직접 비교하기 어려움. 보조정리 전체를 증명해 (w=0)을 얻은 뒤에는 자연어 상한은 0이지만 Lean 상한에는 0이 아닌 항이 남음

대응하는 선언은 NavierStokes/R3/PressureFlux.lean 576행의 exists_uniform_actual_pressure_flux_bound 임

압력 복원 가정 아래 속도 차의 (L^2) 노름, 한 속도장의 (L^3) 노름, 텐서 차 성분의 (L^1) 노름에 대한 시간 구간 전체의 균일 상한을 사용함

exists_uniform_canonicalCutoffFlux_bound, canonicalCutoffFlux_bound에도 유사하지만 동일하지는 않은 상한이 있음

NavierStokes/R3StressPressureEstimate.lean의 regularized_flux_Bound에도 별도의 유사 논증이 있으나, 해당 결과는 컴파일 과정에서 증명될 뿐 제안된 Navier-Stokes 정리의 증명에 직접 사용되지는 않는 것으로 보임

증명 전략의 차이는 세 가지임

자연어 증명은 Riesz 변환의 (L^{3/2}\to L^{3/2}) 유계성을 사용하지만, Lean은 Sobolev 매장으로 (L^2)로 옮긴 뒤 (L^2) 유계성을 사용함. 이 과정에서 필요한 추가 미분이 (A_R)를 도입함

Hölder 부등식에 서로 다른 지수를 사용해 최종 상한도 달라짐

Lean은 좌변 적분의 시간 연속성을 명시적으로 증명해 “거의 모든 시간”을 “모든 시간”으로 강화함

압력 복원과 절단 함수 분해의 차이

보조정리 10.5는 구성된 Navier-Stokes 문제의 두 해 ((v,P)), ((u,p)) 에서 출발해 속도 차가 사라짐을 증명함

자연어 문서는 (w=v-u), (\pi=P-p)로 정의함

Lean은 (w=u-v), (\pi=p-P)를 사용하며, 이후 정의에서도 이 부호 차이를 반영함

절단 함수 (\varphi)는 매끄럽고 콤팩트한 지지집합을 가지며, (0\leq\varphi\leq1)이고 단위 공에서 1임

논문은 Lean 증명과 서술형 PDF 증명이 정확히 일치하지 않는다는 점을 보여줌. 하지만 Lean이 승인한 정리가 Clay Institute의 원래 문제와 동치라면, 이 불일치는 증명 자체의 타당성에 영향을 주지 않음. 다만 문제를 정확히 명시하는 일은 증명만큼 어려울 때도 있으므로, 이 조건은 결코 사소하지 않음. 검증은 두 정리가 동치인지에 집중해야 함.
Lean 증명과 PDF 사이의 간극은 증명을 이해하는 데 방해가 되고, 이해 역시 정당한 목표임. 하지만 이는 증명의 타당성과는 별개임.

적어도 AI 생성 증명 보도는 다른 연구와 마찬가지로 학계가 검토하고 소화할 시간을 갖기 전까지 문제를 풀었다는 ‘주장’으로 다뤄야 함. AI 기업이 동료 심사의 예외라는 생각은 해로움.

내가 이해하기로는 Lean 증명의 정확성이나, 그것이 증명한다고 명시한 추측을 실제로 증명한다는 점에는 이의가 없음. 그것만으로 문제를 해결했다고 볼 수 있으며, 자연어 증명은 있으면 좋은 부가물임.

AI 기업은 동료 심사를 받지 않아도 된다는 생각을 표현한 곳을 본 적이 없는데, 실제로 본 적이 있는지? 지금 이 댓글 타래 자체가 OpenAI의 주장을 검토하는 게시물에 달린 것 아닌지?

AI를 둘러싼 늘 하던 논쟁을 제쳐두면, 핵심은 “형식화된 Lean 증명이 Navier–Stokes 방정식 해의 폭주에 관한 자연어 증명과 대응하지 않는다”는 대목으로 보임.
이를 내가 제대로 이해했다면, 저자들은 LLM이 Navier–Stokes의 원래 자연어 내용을 제대로 형식화하지 못했고, 따라서 OpenAI가 실제로는 Navier–Stokes를 증명하지 못했다고 주장하는 셈임. 사실이라면 Lean 증명은 원래 내용을 잘못 옮긴 다른 명제의 증명일 뿐임. 상당히 대담한 주장인 만큼 다른 연구자들도 동의하는지 궁금함.

그런 주장은 아님. Navier–Stokes의 Lean 형식화가 정확하다는 점에는 아무도 이의를 제기하지 않으므로, 생성된 Lean 증명은 타당하다고 상당히 신뢰할 수 있음.
저자들의 주장은 Lean 증명과 자연어 증명이 서로 다르므로, 자연어 증명의 타당성까지 아직 신뢰해서는 안 된다는 것임. 수학계가 검토해야 할 사안이지만, 학술적 예절 문제를 제쳐두면 Lean 증명만으로도 OpenAI가 상당한 확신을 갖고 증명에 성공했다고 말할 근거는 충분함.

초록을 제대로 이해했다는 전제하에, 증명하지 못했다는 뜻은 아닌 듯함. 자연어와 Lean으로 제시한 두 증명이 서로 동치가 아니라는 뜻으로 읽힘.
그렇다면 Lean 증명은 자연어 증명의 형식 검증이 아니고, 자연어 증명도 Lean 증명을 읽기 쉽게 설명한 것이 아님. 둘 다 바람직한 목표이므로, 각각에 대응하는 증명을 보충하면 총 네 개가 됨.

나는 훨씬 약한 주장으로 읽었음. Lean 증명이 무효라는 것이 아니라, 함께 제공한 PDF의 자연어 증명을 형식화한 결과가 아니라는 것임. 편미분방정식 연구자들이 Lean 증명이 무효라고 하는 것은 듣지 못했고, 오히려 유효하다고 여기는 듯한 이야기를 여러 명에게서 들었음. 과거 수학 연구자였지만 내 전문 분야와는 거리가 멀어 직접 평가할 역량은 부족함.

쟁점은 두 증명의 동치 여부이며, 어느 쪽 증명의 정확성에 대해서도 말하고 있지 않음. 이 부분을 혼동하는 경우가 많은 듯함.

내가 제대로 이해했다면, 자연어 증명과 Lean 증명의 동치 여부를 문제 삼는 것이지 Lean 증명의 정확성을 의심하는 것은 아닌지?

AI가 문제를 풀려고 생성한 자연어 증명과 Lean 증명이 다르다면, Lean 증명이 의도한 주장을 검증하지 않는 것 아닌지?
논문에는 “세 번째 가능성은 자연어 증명이 형식 증명이 실제로 확립한 것보다 더 강한 명제를 제시하며, 당연히 증명도 다른 경우다. OpenAI가 발표한 Navier–Stokes 방정식의 폭주 증명에서 바로 이 일이 발생한다”라고 적혀 있음.

Lean 증명이 정확한지 확인하기는 쉽지만, 우리가 관심 있는 대상을 증명하는지 확인하기는 훨씬 어려움. 코드가 컴파일된다고 버그가 없다고 확신할 수 있는지?

자연어 증명에서도 오류를 찾은 것이 아니라, 두 증명이 다르다는 사실만 찾은 것 아닌지?

자연어 증명은 틀렸지만 Lean 증명은 정확함. 인간도 비슷한 실수를 함. 동작 명세를 작성하고 코드로 옮긴 뒤, 코드가 작동하지 않아 수정하면서 원래 명세는 고치는 것을 잊는 식임.

더 쉽게 증명할 수 있지만 원래 명제와 동치가 아닌 명제는 많음. Lean이 무언가를 증명했다면, 그것이 우리가 실제로 관심 있는 명제인지, 아니면 비슷하지만 결국 다른 질문인지 확인해야 함.

언젠가 의미 이론의 위기에 부딪히게 될지 궁금함. Lean 커널에 버그가 있을 가능성과, 형식화된 명제가 수학자들이 실제로 의도한 것과 다를 가능성을 가정해 볼 수 있음. 그래도 해답보다는 문제의 진술을 확인하는 편이 쉽지 않겠냐는 반론은 자연스러움.
좋은 점은 중간 논증까지 모두 자연어의 의도와 일치할 필요는 없다는 것임. 자연어 증명에서 형식 증명과 미묘하게 다른 대상을 도입하더라도, 원래 명제가 정확히 대응하고 형식 검증을 통과한다면 남는 위험은 Lean 커널뿐임. 이 경우 검증이 무한히 재귀하지는 않음.
하지만 정의란 여전히 기묘하며, 이를 다루는 좋은 이론이 있는지 모르겠음. 질문을 표현하는 데 필요한 서술 능력을 어떻게 정량화할 수 있을지? 수학에서는 정의를 제대로 세우는 것이 어려운 부분일 때가 많은데, 정의 자체가 너무 복잡해져 아무도 의미를 확인할 수 없게 되면 어떻게 될지?
흥미로운 장기 미해결 문제 상당수는 문제 진술이 비교적 간단해서 Lean으로 쉽게 형식화할 수 있어 보임. 그래도 Lean이 만능 해결책인지, 끝없는 토대 확인이 필요한지는 모르겠음. AI의 일반적 지능이 계속 급상승한다면 별로 중요하지 않을 수도 있지만 생각해 볼 만함. 알고리즘 정보 이론(AIT)이 흥미로워지는 지점이기도 하나, 이것이 일반적인 의미론이라고 보지는 않음.

예시의 개괄적인 설명을 보면 오역보다는 형식화 과정에서 LLM이 증명을 수정한 것에 가까워 보임. m+4와 m+5를 오가는 것은 자연어 수학 명제를 해석할 때 흔히 생기는 모호성과는 꽤 다른 일임.

읽어 봐도 OpenAI가 외력이 있는 Navier–Stokes 해의 폭주 대신 실제로 무엇을 증명했는지 명시한 부분은 찾지 못하겠음. 증명 도중 사용한 일부 명제에 대해서는 그런 설명이 있지만, 핵심 결과에 대해서는 보이지 않음.

Lean으로 모든 증명을 검증하는 도구를 만들 수 있다고 생각하는 경우가 많은 듯함. 이것이 왜 불완전성 정리와 충돌하지 않는지 쉽게 설명해 줄 수 있는지?

불완전성 정리는 증명을 어떻게 표현하느냐가 아니라 증명 가능성을 다룬다고 이해함. 괴델 정리의 귀결로, 명제를 받아 증명 가능하면 증명을, 불가능하면 반례를 출력하는 알고리즘은 없다고 알고 있음. 다만 AI 증명기는 언제나 확실한 결과를 내놓는 것이 아니므로 모순은 없다고 봄.

충분히 복잡한 논리 체계에서는 사실상 이 명제에는 증명이 없다라는 명제를 구성할 수 있다는 것이 불완전성 정리의 내용임. 따라서 참이지만 증명할 수 없는 명제가 존재하거나, 거짓인 명제를 증명할 수 있게 됨.

유용한 증명들만 다룬다는 뜻임. 증명에 사용하는 체계에 관한 메타 명제를 만들면 정리의 진술을 얼마든지 더 복잡하고 흥미 없게 만들 수 있음. 어느 수준에 이르면 체계는 자기 자신에 관한 질문에 답할 수 없게 됨.

불완전성 정리는 주어진 공리계 안에서 참도 거짓도 증명할 수 없는 명제가 존재한다는 뜻임. Lean으로 작성할 증명이 이미 있다면, 그 명제는 애초에 그런 증명 불가능성에 해당하지 않음.