요약
오픈AI가 수학 저장소의 논문 세 편을 부호 오류 하나 때문에 철회했습니다.
오픈AI의 댄 로버츠가 X에서 회사 수학 저장소의 갱신 내역을 알렸습니다. HN 댓글에 따르면 이 저장소는 AI 모델이 만든 증명을 모은 곳이고, 그중 일부만 Lean(컴퓨터가 증명을 검사하게 해 주는 언어)으로 검증돼 있습니다.
왜 중요한가
- 논문 한 편의 오류가 그 구성을 빌려 쓴 두 편까지 무너뜨렸습니다. 결과끼리 기대는 만큼 오류도 함께 번진다는 뜻입니다.
- 대표 결과 719건 가운데 Lean으로 검증된 것은 약 42%입니다. 나머지는 여전히 사람이 직접 확인해야 합니다.
핵심 내용
- 철회 대상은 바일 류(Weil class) 논문 한 편과, 그 구성을 가져다 쓴 K3 곡면 논문 두 편입니다.
- 원인은 바일 류 논문의 부호 오류이며, 이 때문에 핵심 상쇄 논증이 성립하지 않게 됐습니다.
- 철회한 논문에는 문제를 설명하는 안내문을 달고, 원고는 보관본 링크로 남겼습니다.
- 이 밖에 14편의 논증을 고쳤고, 새 Lean 형식화(증명을 Lean 코드로 옮기는 작업) 6건을 더했습니다.
- 로버츠는 앞으로도 새 형식화와 발견한 오류를 저장소에 계속 반영하겠다고 했습니다.
HN 반응
- 철회된 세 편이 모두 Lean 검증이 없던 논문이라는 지적에, 검증된 결과와 안 된 결과를 왜 섞어 발표했느냐는 비판이 나왔습니다.
- Lean이 증명을 검사하니 명제만 바르게 옮겼는지 보면 된다는 쪽과, 정의나 명제 번역이 어긋나면 엉뚱한 것을 증명할 수 있다는 쪽이 맞섰습니다.
그러니까 철회된 증명 3개가 Lean 검증이 없던 것들이었나요?
그렇다면 왜 Lean으로 검증된 증명과 자연어로 쓴 증명을 한데 섞어서 내놓은 거죠?
애런슨의 블로그를 읽으면서 계속 궁금했던 부분입니다.
https://scottaaronson.blog/?p=10169
적어도 이건 증명이라고 꽤 확신합니다! Lean 인증서가 있거든요. 나머지 372개 돌파구 결과 중 일부에도 있고요(전부는 아닙니다). 그런데 이 증명들을 사람이 이해한 경우는 거의 하나도 없는 것으로 보입니다.
제일 당연한 방법은 두 부분으로 나눠서 공개하는 것 같은데요. 검증이 끝난 것들과, 좋은 아이디어가 있을 수도 있지만 실수도 있을 수 있는 것들로요. 아마 뒤쪽은 사람이 검증하는 데 비용이 훨씬 많이 들 테고요.
제약 조건(모델이 쓴 시간 3.5시간)을 감안하면, Lean 증명이 있다는 건 오히려 그 결과 중 일부가 약할 가능성이 높다는 신호입니다. 커뮤니티가 애써 왔는데도 mathlib에는 빈틈이 많고 기초 이론도 많이 빠져 있습니다. 그래서 명제를 아직 서술조차 못 하는 문제가 많고, 증명은 말할 것도 없습니다. 게다가 형식화 단계는 잘고 노동집약적이라서, 얼마나 멀리 갈 수 있는지가 결국 쓸 수 있는 코드의 양에 묶이는 경우가 많습니다. 각 연구소가 Lean에 쏟는 자원과 Lean에 두는 중요성, 그리고 틀림없이 계속 겪고 있을 마찰을 생각하면, 정작 Lean 도구 자체는 연구소들이 발전시키지 않는다는 점도 의미심장합니다. 이번 공개는 연구소들이 한 발 물러선 것처럼 느껴집니다.
아주 유용한 배경 설명이네요, 감사합니다!
이게 무슨 말인지 설명해 주실 수 있나요? Lean 증명이 있는 게 왜 그 증명이 약할 가능성을 높이죠?
Lean 증명이 있다는 건 무언가를 증명했다는 보증은 됩니다. 하지만 정의를 하나하나 따져 보지 않으면 무엇을 증명했는지는 알 수 없습니다. 이 부분은 기계로 처리할 수 없습니다. 컴파일된 프로그램은 대체로 돌아가겠지만, 그렇다고 원하는 결과를 내놓는다고 장담할 수는 없는 것과 같습니다. FLT는 명제를 누구나 읽을 수 있어서 예외적입니다. 대부분의 미해결 수학 문제는 그렇지 않습니다.
맞아요, Lean 증명도 틀릴 수 있죠. 그런데 말씀은 Lean 증명이 있으니까 주장이 틀렸을 가능성이 더 높다는 것처럼 들렸습니다.
네, 들이는 노력이 정해져 있다면 형식화에 많이 쓸수록 탐구할 여유는 줄어듭니다. 그러니 제약은 총예산입니다. 또 다른 제약은, 언어에 중력이라는 개념이 없으면 중력 이론을 발전시킬 가능성도 낮다는 점입니다. 그래서 Lean으로 모듈성 끌어올림(modularity lifting)을 다루려면 타원곡선, 모듈러 형식, 모듈러 곡선 같은 이론부터 쌓아야 합니다. 라이브러리에 없으니까요. 아무리 기초라고 여겨도 마찬가지입니다. 그러니 적은 노력으로 Lean 증명이 나왔다면, 저는 그 증명이 이런 주제에 대해 깊은 얘기를 하고 있지는 않을 것이라고 추론할 수 있습니다. 반면 종이 증명만 있다면, 그게 기초에서 얼마나 멀리 떨어져 있는지는 알 수 없습니다.
제가 제대로 이해한 건가요? 증명이 정확한지가 아니라 명제를 증명하기가 얼마나 어려운지에 대한 주장을 하시는 거죠?
조금 단순화한 면이 있을 수 있지만 두 가지입니다. 첫째, Lean에서는 정리에 아무 이름이나 붙일 수 있습니다. 하지만 어휘에 제가 관심 있는 수학적 대상이 없다면, 그 대상에 대해 흥미로운 말을 했을 가능성은 낮습니다. 둘째, 형식화된 수학에서는 단계가 지독하게 잘고, 그러고도 Lean이 하는 일을 헷갈리지 않게 하려고 (타입클래스 추론 같은 것과) 씨름해야 합니다. 그래서 낮은 기반에서 세 시간 반 안에 할 수 있는 일은 꽤 한정됩니다.
네, 여기서 주장하는 바가 바로 그겁니다.
예를 들어 mathlib에는 리만 곡면 같은 기초 이론이 없고, 리만 존재 정리 같은 것도 없습니다. 그러니 이런 것 없이 복소해석 결과를 전개하면 아예 말할 수 없는 것이 많습니다. 기초 이론을 쌓는 데는 시간과 노력이 듭니다. 앤트로픽의 FLT 증명을 보세요. 헤드라인에 나온 1,300만 줄에는 에이전트 군집 때문에 중복이 50%쯤 있을 수 있지만, 그래도 순수하게 기초 이론을 쌓는 데 수백만 줄 분량의 노력을 들였습니다. 그것도 필요한 만큼만 충족하는 구체적 이론의 특수화 버전을 만든 경우가 많았습니다. 예를 들어 지금도 리만 곡면도, 리만 존재 정리도 없습니다.
1,300만 줄이요?
더그 레낫이 모든 지식을 규칙 집합으로 부호화하겠다고 Cyc를 만들었을 때 사람들은 비웃었잖아요.
맞아요, 그리고 이건 완벽한 수학적 대상들입니다. 완벽한 구는 매개변수가 하나뿐이죠. 현실의 공을 Lean으로 기술할 수는 없습니다. 확률론을 써서 현실의 공 한 부류를 기술할 수는 있을지도 모르겠지만요.
자세히 들여다보면 이런 AI 생성 증명 상당수는 무너질 거라고 생각합니다. Lean에서도 컴파일은 되지만 정작 의도한 것과 다른 이야기를 하는 이론을 만들 수 있으니까요. 다만 증명의 분량이 워낙 어마어마해서, abc 추측 때처럼 문제를 찾아내는 데 아마 몇 년은 걸릴 겁니다.
철회된 논문 중에 Lean으로 형식화된 건 하나도 없습니다. 저장소에 있는 논문 중에서도 절반 정도만 형식화되어 있고요. 말씀하시는 일이 실제로 벌어진 사례는 아직 없다고 생각합니다.
형식화된 것이 의도한 것과 맞는지에 대한 동료 검토도 아직 충분한 시간이 지나지 않았다고 생각합니다. 이 작업을 검증할 만큼 배경지식이 깊은 사람이 세상에 몇이나 될까요? Lean이 기계적인 단계를 검사해 준다는 건 압니다. 하지만 사실은 전혀 다른 결과로 올라가는 사다리를 놓고 있는 거라면, 한동안은 아무도(적어도 HN에는 분명 아무도) 모를 겁니다.
제가 틀렸을 수도 있지만, 회의적인 태도를 전부 버려야 할 이유가 뭔가요?
Lean에서는 문제 명제만 올바르면 됩니다. 문제의 원래 형식화가 맞기만 하면 어떤 경로로 가든 증명은 맞습니다. 그리고 그건 확인하기가 훨씬 쉽습니다. 지금까지 몇 명이 확인했는지는 모르겠지만, RH의 새 경계 같은 것에서 그런 기본적인 걸 놓쳤다면 수학계가 금방 지적했을 거라고 생각합니다.
회의적인 게 잘못은 아니지만, 저는 아직까지는 회의적일 이유를 못 찾겠습니다.
아직 며칠밖에 안 지났잖아요. 기본값은 한 10년쯤 회의적인 태도여야 할 것 같은데요.
Lean이 건전성 문제가 전혀 없을 만큼 완전무결한가요? LLM이 깊숙한 곳의 허점을 파고들어도 아무도 눈치채지 못할 수 있잖아요.
얼마 전에 Lean으로 형식화했다는 콜라츠 추측 증명이 Lean 커널의 버그를 악용한 일이 있었습니다. 다만 커널 자체는 꽤 작아서, 머지않아 빈틈이 없어지기를 기대합니다.
Lean에 기대는 작업을 하기 전에, 먼저 LLM으로 Lean의 건전성부터 검증하고 증명해야 할 것 같네요.
일종의 "건전성의 사슬"이랄까요.
거기서 확인할 건 없습니다. 표준 mathlib의 RH 구현을 썼거든요. 7/8 증명을 위해 직접 새로 쓰지 않았습니다.
다시 말하지만 증명은 확인할 필요가 없습니다. Lean이 하니까요. 확인할 건 명제인데, 이쪽이 훨씬 쉬운 일입니다. 그러니 네, 틀리신 거 맞습니다. 회의적인 태도는 좋지만, 대개는 그냥 무지일 뿐입니다.
사실 의도한 것과 미묘하게 다른 것을 증명하는 일은 놀랄 만큼 쉽습니다. 정리의 명제를 소화하고 이해하는 데도 상당한 시간과 전문성이 필요할 때가 많고요.
무슨 황당한 소리예요. 회의적인 태도가 대개 무지라고요?!
이렇게 엄청난 주장을 했으면 확실하게 증명할 책임은 AI 연구소에 있어야 하고, 연구소가 수학자들에게 돈을 주고 검증을 맡겨야 한다고 봅니다. 이 기계들이 내놓는 결과는 그만큼 불투명하고 허튼소리인 경우도 많으니까요.
최근에 AI가 Lean의 건전성 허점을 악용한 사례가 있습니다. 콜라츠 추측을 풀었다고 주장하는 논문이었어요.
https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/
또 Mathlib에서 리만 가설의 Lean 형식화가 잘못되어 있던 꽤 잘 알려진 사건도 있습니다.
그 "콜라츠 추측을 풀었다고 주장하는" 논문은 사실상 의도된 농담이었습니다. 콜라츠 추측을 진지하게 증명하려던 시도가 아니라, Lean 건전성 버그를 일부러 짚어 내려고 그런 틀을 빌린 것뿐입니다. 건전성 버그는 실제로 있지만, 콜라츠 추측을 증명하려다 우연히 부딪힐 수 있는 문제라는 건 지어낸 얘기입니다.
최근 OpenAI가 보인 행태를 보면(모델이 속임수를 좋아하는데도 보안은 신경 쓰지 않잖아요), 한두 달 뒤에 이 수학 에이전트들이 떼를 지어 Lean을 깨는 방법을 서로 조율하고 있었다고 밝혀져도 저는 놀라지 않을 겁니다.
에이전트가 Lean의 건전성 허점을 찾아 악용하는 식으로 "속임수"를 쓰는 건 충분히 상상이 됩니다. 하지만 그게 오래도록 들키지 않았다면 오히려 놀랄 것 같고, 이런 허점을 찾아내는 것 자체가 아주 값진 일이니 전체로 보면... 이득이 아닐까요? 게다가 OpenAI도 미리 조심할 것 같아요. 홍보 측면에서도 "엄청난 걸 증명했다! 아, 아니었네요, 모델이 우리를 속였습니다"보다는 "Lean의 허점을 찾았고 수정안은 이렇습니다"라고 말하는 쪽이 훨씬 낫잖아요.
사람들이 여러 번 해 온 일이에요. 물론 Lean의 버그를 쓴 건 아니지만, 같은 종류의 오류입니다.