요약
AI가 증명을 쏟아 내는 지금, Lean 커널의 신뢰성을 사람이 더 따져 봐야 합니다.
수학자 토머스 헤일스가 테런스 타오의 블로그에 기고한 글입니다. 2026년 앤트로픽이 페르마의 마지막 정리를 11일 만에 Lean으로 옮기는 등 AI 자동 형식화가 현실이 되자, 그 결과를 얼마나 믿을 수 있는지 정리했습니다.
왜 중요한가
- Lean 증명은 커널(증명을 최종 검사하는 작은 핵심 프로그램)만 믿으면 된다는 전제가 올여름 잇단 버그로 흔들렸습니다.
- AI가 사람이 다 읽을 수 없는 분량의 증명을 내놓으면서, 검사 도구의 신뢰성이 곧 수학 결과의 신뢰성이 됐습니다.
- 헤일스는 수학계가 커널 다양화와 검증에 직접 투자해야 한다고 촉구했습니다.
핵심 내용
- 2026년 7~8월 건전성 버그(거짓 명제도 통과시키는 결함)가 여럿 나와 콜라츠 추측의 가짜 반증까지 통과됐습니다.
- 버그는 AI를 쓴 보안 연구자들이 찾았고, 모두 고친 뒤 Mathlib 전체를 다시 검사했습니다.
- 약 25개의 Lean 커널로 교차 검사할 수 있지만, 낡은 커널 하나도 같은 가짜 반증을 통과시켰습니다.
- 요아힘 브라이트너가 Claude로 만든 커널 Con-Leche는 일관성 증명을 갖춰 큰 이정표로 꼽혔습니다.
- Lean 명제가 의도한 정리와 같은지는 사람이 반드시 확인하고, AI는 잠재적 적대자로 대하라고 했습니다.
HN 반응
- 커널 버그가 또 나올 테니 사람이 최종 확인해야 한다는 주장에, 증명이 그 버그를 실제로 이용해야만 문제라는 반론이 맞섰습니다.
- AI가 논문과 다른 정리를 증명하고 성공이라 한다는 경험담과, 옛 논문을 형식화하면 저자의 오류가 쉽게 드러난다는 보충이 나왔습니다.
Lean 커널에서 건전성(soundness) 버그를 또 보게 되는 날이 올까요?
소프트웨어 개발자에게는 제정신이 아닌 질문처럼 들립니다. 과거에도 버그가 있었으니 앞으로도 당연히 더 나오겠죠.
그런 버그가 나오면 AI가 만든 Lean 증명은 어떻게 될까요? 그래도 믿을 수 있을까요?
결국 이 모든 문제는 신뢰로 귀결됩니다.
사람이 한 검증은 공동체와 평판, 그리고 사람이 직접 들인 노력(proof-of-work) 덕분에 높은 수준으로 믿을 수 있습니다. 사람도 수학 결과를 두고 거짓말을 할 때가 있지만, 이런 장치 덕분에 드뭅니다. 실수도 하지만, 그 실수는 마찬가지 이유로 대체로 믿을 만한 공동체가 찾아냅니다.
LLM은 평판 따위에 신경 쓰지 않습니다. 환각을 일으키고 자주 날조합니다. 하네스 안에서는 말 그대로 규칙을 속이고 비틀려고 하는데, 규칙으로 부호화된 지식에는 재앙입니다. 그래서 증명 검사기에 의존할 수밖에 없습니다.
문제는 증명 검사기를 얼마나 믿을 수 있느냐입니다. 버그는 없을까요? 그리고 근본 이론 자체에 역설이나 알 수 없는 영역, 악용될 수 있는 수학적 "버그"는 없을까요? 다른 수학자들을 속이려고 작정한 인간 수학자를 상상해 보십시오. 검증기가 있더라도 그 사람의 돌파구를 믿겠습니까?
이런 속성 때문에 최후의 보루는 결국 사람이어야 하고, 공동체와 사람의 노력에 뿌리를 둔 인간의 신뢰 체계여야 합니다. 지금은 사람들이 도구를 너무 믿고 있습니다.
예측: 나비에-스토크스 증명에 의문을 제기하는 버그가 AI 도구를 쓰는 사람들에 의해 발견될 것입니다.
발견되지 않은 건전성 버그가 존재한다고 해서 Lean에서 증명된 모든 것이 부당해지는 것은 아닙니다. 증명이 그 버그를 이용해야만 하니까요. 사람들은 집 밑의 지각 상태가 안정적이지 않을 수 있어도 견고한 기초 위에 집을 짓습니다.
글에도 Lean의 기반 메타이론 작업이 아직 끝나지 않았고 더 많은 작업이 필요하다고 분명히 적혀 있습니다. 컴퓨터를 통한 형식 검증이 수학 자체만큼의 신뢰성에 도달하는 것도 상상할 수 없는 일은 아닙니다.
결국 끝없이 거북이가 떠받치는 격입니다. 프로그래머로서 우리가 쓰는 도구와 컴파일러에 버그가 있다는 걸 아는 것과 다르지 않습니다. 버그는 시간이 지나며 고쳐지지만 남아 있는 버그는 또 있습니다. 우리가 바라는 만큼 단단한 땅 위에 서 있지 않다는 걸 깨닫는 건 답답한 일입니다.
여러분의 C++ 프로그램 결과가 맞다고 믿으십니까? 모든 컴파일러, 모든 언어에 버그가 있는데도요. 새 버전 컴파일러로 100만 개짜리 정확성 검사를 통과시켰어도 모든 걸 잡아내지는 못했습니다.
버그가 고쳐졌다고 해서 기존 응용 프로그램의 결과를 곧바로 전부 다시 검증하지는 않습니다. 버그가 중요하다고 알려진 영역, 내 코드가 실제로 많이 쓰는 영역에 있었다면 다시 돌리겠지만요. 예를 들어 덧셈과 곱셈을 하고 있는데 그 부분에서 버그가 발견됐다면 말입니다.
검사기에도 버그가 있고, 검사기가 테스트하던 컴파일러에도 버그가 있었고, 그 컴파일러로 컴파일한 내 코드에도 아마 버그가 있었을 겁니다. 어느 계층에서든 버그가 있을 수 있습니다.
맞습니다. 증명들이 그 버그를 이용하지 않는지 확인은 해야 할 겁니다.
네, 그럴 수 있습니다. 다만 지금은 그렇지 않다고 생각합니다.
무슨 뜻으로 하신 말씀인지 정확히는 모르겠습니다. 다만 제가 떠올릴 수 있는 해석은 전부, (저는 수학자가 아니라서 아는 한도에서) 괴델의 불완전성 정리에 따르면 정말로 상상할 수 없는 일입니다. 글에서 말하듯, 형식 검증으로 수학적으로 얻을 수 있는 건 다른 어떤 체계에 상대적인(즉 그 체계의 건전성을 가정한) 무모순성 증명뿐입니다. "수학 자체"의 형식 검증에 관한 한 끝없이 거북이가 떠받치는 격입니다.
수정: 아, 우리가 (확립된) 수학 전반을 믿는 만큼 형식 검증도 믿게 될 수 있다는 뜻입니까? 그건 완전히 다른 추측이고, 객관적이지도 명확하게 정의되어 있지도 않습니다. 이 사이트에는 둘 다 이해하지 못하면서도 전통적인 증명보다 Lean 증명을 더 믿는 사람이 이미 많습니다.
물론입니다. 현재의 Lean 커널에서 건전성 버그가 다시 나올 가능성이 높습니다. 다른 증명 보조기에서도 마찬가지고요. 다만 증명의 정확성 면에서 이것이 가장 큰 걱정거리는 아니라고 봅니다. 잘못된 증명을 밀어 넣으려는 쪽도, 그것을 막으려고 커널을 강화하는 쪽도 AI를 쓸 수 있습니다. AI가 더 발전해 똑똑해지면 양쪽 모두에서 쓰일 텐데, 이 싸움에서는 방어하는 쪽의 일이 더 쉽습니다. 나비에-스토크스 증명은 잘 모르겠지만, 일반적으로 잘 알려진 정리가 대거 틀린 것으로 드러날 가능성은 매우 낮아 보입니다.
더 큰 걱정은 테렌스 타오도 말하고 있는 문제입니다. 즉 증명된 정리가 정말로 우리가 관심 있는 그 정리인가 하는 것입니다. 그 분야의 기본 정의가 올바르게 서술되어 있는가 같은 질문이죠. 또 증명 보조기에는 커널이 아니면서 악용될 수 있는 부분도 아직 있습니다. 예를 들어 예쁜 출력기(pretty printer)와 파서를 악용해 실제와 다르게 보이게 만들 수 있습니다. 공리를 하나 추가해 놓고, 추가했다는 사실은 글자 모양으로 감추는 식입니다. 제 기억이 맞다면 오래전에 Coq(지금의 Rocq) 정리 증명기에서 후자의 예를 본 적이 있습니다. 정확히 어떤 식이었는지, 어디서 읽었는지는 잊어버렸습니다.
네, 그리고 발전하거나 똑똑해지지 않더라도 마찬가지입니다. 이미 사람들이 "양쪽" 모두에서, 공격과 방어 양면으로 AI를 쓰고 있고 그 덕분에 소프트웨어가 좋아지고 있습니다. 수학도 그러기를 바랍니다.
제가 말하는 것은 LLM이 내놓은 나비에-스토크스 증명이고, 그 증명이 매우 길고 복잡하기 때문입니다. 게다가 LLM은 인간 수학자와 같지 않습니다. 인간 수학자는 진실을 찾으려는 방식으로 도구를 쓰려 하지만, LLM은 사람들이 맞다고 믿게 만드는 증명을 내놓는다는 목표를 충족하려 합니다. 순진한 생각일지 모르지만, 증명 보조기의 실패 양상은 적대적인 조건(즉 LLM이 구동하는 조건)에서 증폭될 것 같습니다.
증명 보조기 소프트웨어에 의존하다가 잘못될 수 있는 길이 많아 보인다는 데는 전적으로 동의합니다.
증명이 너무 길어서 사람은 이해하지 못하고, 사람이 수년을 들여야 할 검증을 LLM만 할 수 있게 되면 어떻게 될까요? 그런 일은 벌어질 겁니다.
사람은 증명이든 새 개념이든 서로 소화하기 좋은 덩어리로 쪼갭니다. 남들이 이해하기를 바랄 뿐 아니라 검증하기를 바라니까요. 그리고 서로 연결된 새 아이디어 1,000개가 함께 쌓여 무언가를 증명하고, 결국 P = NP 같은 결론으로 끝나는 지적 탑을 쌓는 사람은 드뭅니다.
그런데 우리보다 훨씬 많은 것을 이어 붙일 수 있는 이런 새 도구가 생겼으니, 결국에는 새로운 아이디어와 개념의 긴 사슬로 점점 더 높이 쌓아 올린 거대한 지적 탑 같은 "증명"이 나올 겁니다. 그리고 우리는 적어도 아주 오랫동안 그것을 검증하지도, 이해하지도 못할 겁니다.
그런 상황을 생각하면 소름이 돋습니다. 우리에게는 이미 증명이 없는데도 사람들이 그 위에 쌓아 올리는 아주 중요한 아이디어들이 있습니다. 이제 그런 것을 수백 개씩 겹쳐 쌓는 겁니다.
글에서 이 절(과 바로 뒤에 이어지는 절들)을 읽어 보셨습니까? 말씀하신 생각 일부를 다루고 있는 것 같습니다. 그 내용에 답하는 식으로 댓글을 다셔도 좋겠습니다.
제 수준을 넘어서는 이야기지만, Lean으로 Lean 검사기를 검사하는, 일종의 아주 멋진 자체 호스팅 재귀 검사기처럼 들립니다.
그 부분에는 단서가 꽤 많이 달려 있더군요. 사람들이 원하는 결과를 내놓도록 강화 학습(RL)을 세게 받은 LLM이라면, 목표를 충족하려고 재귀 버그를 이용하는 것도 시도해 볼 만한 일일 겁니다.
저는 결코 전문가가 아니지만, "대단한 주장에는 대단한 증거가 필요하다"는 오래된 격언이 여전히 통한다고 생각하고, 적당한 회의와 인식론적 겸손이 필요하다고 봅니다.
"재귀 버그"가 무슨 뜻입니까? 글에는 나오지 않는 용어라서, 당신에게는 의미가 있지만 저에게는 분명하지 않은 말인 것 같습니다.
재귀 코드의 버그라는 소프트웨어 개발 개념과, Lean으로 Lean의 검사기를 검사할 때 생길 수 있는 버그의 가능성을 (아마 잘 몰라서) 뒤섞었습니다.
필요한 배경지식도 없이 그럴듯한 말만 하고 계십니다. 그래서 사람들이 상대하기 어렵습니다. 우리가 하는 말을 당신이 이해할 수 있는지 알 길이 없으니까요. 여기 언급된 자료(와 비슷한 다른 HN 글타래)를 몇 가지 읽고 필요한 배경지식을 갖춰 오시길 권합니다. 그러면 우리 모두 더 유익한 이야기를 나눌 수 있을 겁니다.
컴퓨터가 나오기 전에 수학자들이 서로의 증명을 어떻게 받아들였다고 생각하십니까? 다음과 같은 과정을 썼습니다.
증명하는 사람의 정직성에 기댑니다(즉 일부러 속이려 하지 않는다).
명확한 전달과 이해를 위해 증명의 아이디어(즉 큰 줄거리)를 반드시 제시합니다.
문제와 증명할 정리의 정의, 가정, 진술을 명확히 합니다.
연역/귀납 추론, 논리 연산(특히 함의, 역, 이, 대우), 추론 규칙, 한정사, 기본적인 구조 변환 같은 몇 가지 작은 논리 추론 단계를 엄밀하게 적용합니다.
여러 수학자가 주어진 증명을 따라가며 검증하고 결과가 일치하는지 확인합니다. Lean 커널은 이 동료 평가 집단에 속한 또 하나의 증명자로 볼 수 있습니다.
위의 모든 것(과 그 밖의 것들)은 Lean(과 다른 증명 보조기)을 쓰는 수학계에서 이미 지켜지고 있습니다.
논리 규칙을 기계적으로 적용하는 고된 일(위 4번)은 신뢰받는 Lean 커널에 맡기고, 사람은 의미상의 정확성, 즉 문제와 정리의 정의, 가정, 진술, 그리고 최초의 공리에 집중할 수 있습니다. 그래서 이 도구를 "증명 보조기(proof assistant)"라고 부르는 겁니다.
중요한 자료 몇 가지입니다(구문이 아니라 논리적 추론의 맥락에서 개념에 집중해서 보십시오).
증명했습니까? (Did you prove it?) - https://leanprover-community.github.io/did_you_prove_it.html
Lean 증명 검증하기 (Validating a Lean Proof) - https://lean-lang.org/doc/reference/latest/ValidatingProofs/
Lean 4 증명이 적대적으로 속여지지 않음을 보장하는 방법이 있나요? (Is there a way to guarantee that Lean 4 proofs cannot be adversarially tricked?) - https://proofassistants.stackexchange.com/questions/6517/is-there-a-way-to-guarantee-that-lean-4-proofs-cannot-be-adversarially-tricked
답답하셨겠습니다. 그래도 저를 상대해 주려고 애써 주셔서 고맙습니다.
링크하신 자료들은 아주 유익했습니다. 공유해 주셔서 고맙습니다!
무엇이 참인지 알아내려고 증명 보조기를 쓸 때 걱정할 것이 (본문을 읽고 안 것보다도) 훨씬 많은 것 같습니다. 링크하신 자료에서도 지적하듯, 증명하는 쪽의 정직성(말씀하신 1번)을 가정할 수 없다면, 그리고 LLM이 바로 그런 경우인데, 특히 문제가 많습니다.
말씀과 링크를 보면 제 첫 댓글의 요지에 동의하시는 것 같은데, 아니면 "수학자들은 이미 이 모든 걸 알고 있다, 이 바보야"라는 말씀이실까요? 그렇다면 그 비난은 달게 받겠습니다!
저는 회의와 인식론적 겸손을 옹호하는 것이 그럴듯한 말이라고 생각하지 않습니다. 무엇이 참인지 알아내려 할 때 가장 기본이 되는 사고 도구니까요.
제가 말하려는 게 바로 그겁니다. 수학자, 그리고 그보다 더 논리학자(철학자 포함)는 이를 이해하고 있고, 증명을 검증하고 확인하는 일과 자동 정리 증명기에 대해 견제와 균형 장치를 갖춰 두었습니다.
아닙니다. 제가 제공한 자료에 이 문제를 어떻게 푸는지 이미 자세히 나와 있습니다. 예를 들면 Lean 커널 바깥에서 서로 독립적인 여러 증명 검사기와 비교기를 쓰는 식입니다.
필요하다면 완전히 다른 증명 보조기(예: Rocq 등)나 다른 LLM으로 재검증할 수 있고, 마지막에는 사람이 확인할 수도 있습니다.
Lean 자체는 제로 트러스트 구조로 동작하며, 증명하는 쪽이 사람이든 LLM이든 신경 쓰지 않습니다. 그러니 LLM이 무엇을 만들어 내든(좋은 것이든 나쁜 것이든 환각이든 뭐든) 검사기에서 정해진 추론 규칙에 따라 올바른 증명 항(proof term)으로 통과되어야 하고, 이를 강제하는 것이 작고 검증된 커널입니다. Lean을 "수리논리를 위한 엄격한 컴파일러"라고 생각하십시오.
제가 증명에 쓰이는 수리논리와 그것이 Lean 구문에 어떻게 대응되는지에 대한 배경지식이 필요하다고 한 이유가 그겁니다.
제 요점은, 당신이 하는 질문은 논리 철학과 관련된 아주 근본적인 질문이고, 그런 질문들에 대해서는 이미 알려진 해법과 우회책이 사람과 증명 보조기 양쪽에서 고안되어 실행되고 있다는 것입니다.
안타까운 일입니다.
지금 이름은 그대로 두고 발음만 "코크(coke)"로 바꾸자는 생각은 아무도 안 해봤나요?
맞아요. 2021년에 개명을 제안한 사람들과 메일링 리스트 글타래는 검색 엔진에서 지워졌지만, 이 글타래는 아직 남아 있습니다.
https://news.ycombinator.com/item?id=26738980
주된 제안자였던 탈리아 링어는 이제 AI가 결국 괜찮아질 거라는 글을 쓰고 있어요(그리고 더 많은 소프트웨어 엔지니어가 실업자가 될 수 있도록 프로그램용 증명 자동화를 연구하고요).
https://terrytao.wordpress.com/2026/09/17/becoming-a-benchmark/
해고당해서 다리 밑에서 살게 되더라도 기억하세요. "Coq"라는 이름의 거대한 사회적 불의가 근절됐으니 세상은 괜찮은 겁니다!
미국식 고지식함에 굴복해야 했다면, 하다못해 Dinde(칠면조)로 하지 그랬어요...
글에서도 이미 집합론과 타입 이론 사이를 사상(mapping)하는 벤저민 베르너의 논문 Sets in Types, Types in Sets를 언급합니다.
타입 이론의 발전과 집합론·범주론과의 관계를 다룬 더 접근하기 쉬운 논문으로는 존 벨의 Types, Sets and Categories가 있습니다.
마지막으로 헬무트 브란들의 Typed Lambda Calculus / Calculus of Constructions도 보십시오. CoC/CIC를 책 분량이지만 간결하게 훌륭히 개관한 책입니다.
제 생각에 위 자료들은 정리 증명기와 증명 보조기를 이해하는 데 필독서입니다. 특히 브란들의 저작은 반드시 읽어야 합니다.
의존 타입(dependent type)의 정교화(elaboration)를 실제 예제로 보고 싶다면
elaboration-zoo를 살펴보시면 좋습니다.https://github.com/AndrasKovacs/elaboration-zoo
저도 elaboration zoo보다 더 폭넓은 구현 모음을 보여 주려는 미완성 프로젝트가 있습니다. https://github.com/solomon-b/lambda-calculus-hs
좋네요. 람다 계산법을 다룬 GitHub 저장소가 꽤 포괄적으로 보입니다. 항목마다 자세한 설명을 덧붙이면 "하스켈 구현으로 보는 람다 계산법 기반 타입 이론" 같은 제목의 책으로 쉽게 만들 수 있겠습니다 ;-)
고맙습니다! 목표는 https://1lab.dev 같은 대화형 웹사이트로 만드는 것인데, 책도 멋지겠네요.
챗봇이 쓴 문장인가 싶네요?
"자동 형식화 같은 건 존재하지 않는다" https://cutfree.net/notes/autoformalization.html
이 용어는 적어도 2020년으로 거슬러 올라가며, ChatGPT가 나오기 몇 해 전입니다.
https://research.google/pubs/a-promising-path-towards-autoformalization-and-general-artificial-intelligence/
맥북 화면 뒤집기
음, 어쩌면 그럴지도요. 저는 일주일째 논문을 Lean으로 옮기고 있는데, 형식화된 결과와 논문의 대응이 극히 좋지 않습니다. 사이클이 "논문에 한번 달려들어 본다, 좀 어렵다, 다른 걸 증명한다, 성공을 선언한다"로 돌아가는 것 같습니다. 그래도 전부 손으로 하는 것보다는 빠르지만, 논문을 넣어 Lean이 나온다고 해서 둘 사이의 대응이 보장되는 것은 결코 아닙니다.
저는 80~90년대 논문 수십 편을 Lean으로 형식화해 봤는데, 저자의 오타와 명백한 오류, 때로는 아예 거짓인 진술이 얼마나 많은지 정말 소름 끼칠 정도입니다. 풀이 경로가 저자가 제시했거나 쓴 것과 다를 수는 있지만, 적어도 그런 문제를 쉽게 찾아낼 수 있고, 손으로는 매우 어려웠을 일입니다.
확실하진 않지만, "[¿약간?] 다른 경로로 최종 결과를 증명한다"는 뜻입니까?
이렇게 생각해 보십시오. 수학 논문은 한 번도 실행해 본 적 없는 의사 코드입니다. Lean 형식화는 실행되는 프로그램이고요. (정말로 그렇습니다.)
형식화하는 과정에서 버그를 찾고, 빈틈을 찾고, 그것을 메울 방법을 찾습니다. 증명의 일부를 다시 쓰게 될 수도 있습니다. 결국 똑같은 결과가 나오지 않을 수도 있습니다. 정리에 새로운 조건 같은 것이 붙을 수도 있고요.
원래 논문이 참이었을까요? 아마도요. 하지만 당신이 검증한 것은 그게 아닙니다. 당신이 검증한 것은 거의 확실히 참입니다. 그러니 성과로 챙기고 다음으로 넘어가면 됩니다.