상금 100만 달러가 걸린 나비에–스토크스 난제에 AI가 답을 찾았다는 발표. 수학자들은 증명과 그 증명을 검사한 방식까지 다시 들여다보고 있다.
본문
컵 안의 커피를 숟가락으로 저으면 작은 소용돌이가 생긴다. 손을 멈춰도 잠시 돌다가 잦아든다. 비행기 주변의 공기부터 혈관을 지나는 피까지, 이렇게 흐르는 것을 설명할 때 등장하는 이름이 나비에–스토크스 방정식이다. 오래전부터 사용해 온 식이지만, 주어진 조건에서 그 식의 해가 시간이 지나도 매끄럽게 유지되는지는 여전히 어려운 수학 문제다.
이 문제에는 상금 100만 달러가 걸려 있다. 클레이 수학연구소가 2000년 선정한 밀레니엄 난제 일곱 개 중 하나다. 각 문제의 해결에 100만 달러씩을 배정했다. 익숙한 물의 움직임을 설명하는 식이, 수학자들에게는 거액의 상금이 걸린 질문으로 남아 있었던 셈이다.
그 질문에 AI가 답을 찾았다는 발표가 나왔다. 하지만 발표문과 검증 논쟁을 따라가면 상금보다 먼저 살펴야 할 것이 보인다. 컴퓨터가 증명을 확인했다는 말은 정확히 어디까지 확인했다는 뜻일까.
## 이미 쓰는 식에도 모르는 것이 있다
나비에–스토크스 방정식은 유체의 움직임을 수학으로 표현한다. 그렇다고 밀레니엄 난제가 그 식을 처음 만들거나 특정 비행기의 공기 흐름을 한 번 계산하는 문제인 것은 아니다. 충분히 매끄럽게 시작한 3차원 유체의 움직임이 시간이 지나도 매끄럽게 유지되는지, 아니면 어느 순간 해가 무너지는 경우가 있는지를 묻는다.
물을 개별 분자 하나하나로 추적하지 않고 연속된 물질처럼 다룬다는 점도 중요하다. 수학적 해에서 어떤 양이 끝없이 커진다고 해서 실제 커피가 무한한 속도로 튄다는 뜻은 아니다. 식이 표현하는 이상화된 세계와 실제 물질의 움직임 사이에는 간격이 있다.
## 발표와 확정 사이
OpenAI는 9월 8일 내부 AI 시스템이 유체 방정식의 해가 유한한 시간 안에 특이점을 만드는 증명을 찾았다고 발표했다. 외부 힘이 작용하는 조건의 결과이며, 회사는 이것이 공식 문제의 C와 D 항목을 해결한다고 주장했다. 사람이 읽는 증명문과 컴퓨터가 검사할 수 있는 Lean 형식의 증명을 함께 공개했다.
클레이 수학연구소도 9월 11일 성명에서 해결 발표에 대한 기대를 드러냈다. 그러면서 성과를 평가하고 공로를 판단하는 과정은 서두르지 않는다고 밝혔다. 10월 15일 확인한 문제 페이지는 여전히 Active로 표시돼 있다.
상금도 발표와 동시에 지급되는 방식이 아니다. 연구소가 인정하는 출판 경로에 결과를 발표하고, 그 뒤 최소 2년이 지나며, 세계 수학계의 일반적인 인정을 받아야 심사 대상으로 고려된다. OpenAI는 이번 결과로 밀레니엄 상을 청구할 의도가 없다고 밝혔다. 100만 달러짜리 질문에 답했다고 발표한 것이지, AI가 이미 상금을 받았다는 이야기는 아니다.
## 번역된 증명이 원래 증명과 같을까
논란을 이해할 실마리 가운데 하나는 ‘번역’이다. Lean은 수학 문장을 정해진 형식으로 표현하고, 그 형식 안에서 추론이 성립하는지 기계적으로 검사하는 도구다. 그런데 사람이 쓴 문장을 그 언어로 옮길 때, 조건 하나가 빠지거나 뜻이 달라지면 어떻게 될까. 검사를 통과한 문장이 원래 확인하려던 문장과 같은지도 살펴야 한다.
10월 6일 공개된 알렉산더 바스투니스·파비안 치르첼리·안데르스 한센의 논문은 바로 이 틈을 지적한다. 연구자들은 OpenAI의 나비에–스토크스 증명을 사례로 들며, 자연어 증명과 Lean으로 형식화된 증명이 대응하지 않는다고 주장했다. 아직 학술지 심사를 마친 결과로 소개할 수 없는 공개 논문이며, 그 주장을 수학계 전체의 최종 판정으로 확대하지 않는다.
그렇다고 컴퓨터 검사가 쓸모없다는 이야기도 아니다. 무엇을 검사하도록 입력했는지까지 확인해야 한다는 이야기다. 계산기에서 정답이 나와도 처음 입력한 식이 문제에 적힌 식과 같은지는 다시 보는 것과 닮았다. 실제 수학적 번역은 그 비유보다 훨씬 복잡하지만, 두 단계가 따로 있다는 점은 이해할 수 있다.
컵 안의 소용돌이는 잠시 후 잦아들지만, 그 움직임을 끝까지 설명하는 증명을 둘러싼 논쟁은 이어진다. 100만 달러의 상금 앞에 지금 놓인 것은 수표보다 두 종류의 문서다. 사람이 읽는 증명과 컴퓨터가 검사한 증명. 두 문서가 같은 질문에 같은 답을 하는지, 수학자들이 다시 펼쳐 보고 있다.
확인 자료
OpenAI · 나비에–스토크스 해결 발표
https://openai.com/index/navier-stokes-solution/
클레이 수학연구소 · 나비에–스토크스 문제
https://www.claymath.org/millennium/navier-stokes-equation/
클레이 수학연구소 · 상금과 해결 발표에 대한 성명
https://www.claymath.org/news/navier-stokes-announcement/
클레이 수학연구소 · 밀레니엄 상 규정
https://www.claymath.org/millennium-problems/rules/
Bastounis·Circelli·Hansen · AI 형식화 비판 논문
https://arxiv.org/abs/2610.08144
편집: 사실은 위 자료를 대조해 확인했으며, 해석은 MUADAILY의 편집 관점입니다. 이미지: MUADAILY · AI 생성 설명용 이미지. 실제 실험 사진이나 검증된 수치 계산 결과가 아님.
이 문제에는 상금 100만 달러가 걸려 있다. 클레이 수학연구소가 2000년 선정한 밀레니엄 난제 일곱 개 중 하나다. 각 문제의 해결에 100만 달러씩을 배정했다. 익숙한 물의 움직임을 설명하는 식이, 수학자들에게는 거액의 상금이 걸린 질문으로 남아 있었던 셈이다.
그 질문에 AI가 답을 찾았다는 발표가 나왔다. 하지만 발표문과 검증 논쟁을 따라가면 상금보다 먼저 살펴야 할 것이 보인다. 컴퓨터가 증명을 확인했다는 말은 정확히 어디까지 확인했다는 뜻일까.
## 이미 쓰는 식에도 모르는 것이 있다
나비에–스토크스 방정식은 유체의 움직임을 수학으로 표현한다. 그렇다고 밀레니엄 난제가 그 식을 처음 만들거나 특정 비행기의 공기 흐름을 한 번 계산하는 문제인 것은 아니다. 충분히 매끄럽게 시작한 3차원 유체의 움직임이 시간이 지나도 매끄럽게 유지되는지, 아니면 어느 순간 해가 무너지는 경우가 있는지를 묻는다.
물을 개별 분자 하나하나로 추적하지 않고 연속된 물질처럼 다룬다는 점도 중요하다. 수학적 해에서 어떤 양이 끝없이 커진다고 해서 실제 커피가 무한한 속도로 튄다는 뜻은 아니다. 식이 표현하는 이상화된 세계와 실제 물질의 움직임 사이에는 간격이 있다.
## 발표와 확정 사이
OpenAI는 9월 8일 내부 AI 시스템이 유체 방정식의 해가 유한한 시간 안에 특이점을 만드는 증명을 찾았다고 발표했다. 외부 힘이 작용하는 조건의 결과이며, 회사는 이것이 공식 문제의 C와 D 항목을 해결한다고 주장했다. 사람이 읽는 증명문과 컴퓨터가 검사할 수 있는 Lean 형식의 증명을 함께 공개했다.
클레이 수학연구소도 9월 11일 성명에서 해결 발표에 대한 기대를 드러냈다. 그러면서 성과를 평가하고 공로를 판단하는 과정은 서두르지 않는다고 밝혔다. 10월 15일 확인한 문제 페이지는 여전히 Active로 표시돼 있다.
상금도 발표와 동시에 지급되는 방식이 아니다. 연구소가 인정하는 출판 경로에 결과를 발표하고, 그 뒤 최소 2년이 지나며, 세계 수학계의 일반적인 인정을 받아야 심사 대상으로 고려된다. OpenAI는 이번 결과로 밀레니엄 상을 청구할 의도가 없다고 밝혔다. 100만 달러짜리 질문에 답했다고 발표한 것이지, AI가 이미 상금을 받았다는 이야기는 아니다.
## 번역된 증명이 원래 증명과 같을까
논란을 이해할 실마리 가운데 하나는 ‘번역’이다. Lean은 수학 문장을 정해진 형식으로 표현하고, 그 형식 안에서 추론이 성립하는지 기계적으로 검사하는 도구다. 그런데 사람이 쓴 문장을 그 언어로 옮길 때, 조건 하나가 빠지거나 뜻이 달라지면 어떻게 될까. 검사를 통과한 문장이 원래 확인하려던 문장과 같은지도 살펴야 한다.
10월 6일 공개된 알렉산더 바스투니스·파비안 치르첼리·안데르스 한센의 논문은 바로 이 틈을 지적한다. 연구자들은 OpenAI의 나비에–스토크스 증명을 사례로 들며, 자연어 증명과 Lean으로 형식화된 증명이 대응하지 않는다고 주장했다. 아직 학술지 심사를 마친 결과로 소개할 수 없는 공개 논문이며, 그 주장을 수학계 전체의 최종 판정으로 확대하지 않는다.
그렇다고 컴퓨터 검사가 쓸모없다는 이야기도 아니다. 무엇을 검사하도록 입력했는지까지 확인해야 한다는 이야기다. 계산기에서 정답이 나와도 처음 입력한 식이 문제에 적힌 식과 같은지는 다시 보는 것과 닮았다. 실제 수학적 번역은 그 비유보다 훨씬 복잡하지만, 두 단계가 따로 있다는 점은 이해할 수 있다.
컵 안의 소용돌이는 잠시 후 잦아들지만, 그 움직임을 끝까지 설명하는 증명을 둘러싼 논쟁은 이어진다. 100만 달러의 상금 앞에 지금 놓인 것은 수표보다 두 종류의 문서다. 사람이 읽는 증명과 컴퓨터가 검사한 증명. 두 문서가 같은 질문에 같은 답을 하는지, 수학자들이 다시 펼쳐 보고 있다.
확인 자료
OpenAI · 나비에–스토크스 해결 발표
https://openai.com/index/navier-stokes-solution/
클레이 수학연구소 · 나비에–스토크스 문제
https://www.claymath.org/millennium/navier-stokes-equation/
클레이 수학연구소 · 상금과 해결 발표에 대한 성명
https://www.claymath.org/news/navier-stokes-announcement/
클레이 수학연구소 · 밀레니엄 상 규정
https://www.claymath.org/millennium-problems/rules/
Bastounis·Circelli·Hansen · AI 형식화 비판 논문
https://arxiv.org/abs/2610.08144
편집: 사실은 위 자료를 대조해 확인했으며, 해석은 MUADAILY의 편집 관점입니다. 이미지: MUADAILY · AI 생성 설명용 이미지. 실제 실험 사진이나 검증된 수치 계산 결과가 아님.
편집 안내
본문의 출처 링크는 새 창으로 열립니다.
