수학자가 Lean 정리 증명기에 알아야 할 것: 신뢰성과 AI

AI 요약

Thomas Hales는 수학의 일관성과 신뢰성이 과학과 문명에 중요하다는 관점에서 Lean theorem prover의 형식화, AI 자동 형식화, 검증 신뢰성을 설명합니다. 형식 증명은 수학의 기초와 논리 규칙 수준에서 컴퓨터로 검사하는 증명입니다. 4색 정리, Feit–Thompson 정리, 케플러 추측, 페르마의 마지막 정리 등이 형식화됐고, Lean의 수학 라이브러리 mathlib에는 약 30만 개의 정리, 10만 개가 넘는 정의, 250만 줄의 코드와 700명이 넘는 기여자가 있다고 소개합니다.

AI 자동 형식화의 진전

논문이나 교과서의 수학을 AI가 Lean 등의 증명 보조기에서 검사할 수 있는 코드로 바꾸는 작업을 autoformalization이라고 부릅니다. Hales가 소개한 사례에는 소수 정리 형식화 지원, Munkres 위상수학 교재 일부를 2주 동안 형식화한 프로젝트, 24차원 구 포장 문제의 약 50만 줄 형식화와 이후 약 20만 줄로 줄인 작업, Meta의 ATLAS 프로젝트가 있습니다. Anthropic은 2026년 페르마의 마지막 정리 형식화에 11일 동안 Lean 코드 1,300만 줄을 생성했다고 발표했고, OpenAI는 나비에-스토크스 강제 발산 결과의 형식화를 공개했습니다.

다만 증명 코드가 커널 검사를 통과했다는 사실만으로 원 논문의 정리를 증명했다고 단정할 수는 없습니다. 형식화 과정에서 명제나 정의가 원문과 다르게 바뀌지 않았는지 사람이 대조해야 합니다. Hales는 Lean의 comparator 도구가 이런 점검과 승인되지 않은 공리 사용 여부 확인을 돕는다고 설명합니다.

Lean의 신뢰 경계와 soundness bug

Lean은 프로그래밍 언어이자 수학 표현 언어입니다. 작성한 증명 스크립트는 elaboration 과정을 거쳐 증명 항으로 변환되고, Lean kernel이 그 결과를 검사합니다. 커널이 잘못된 증명을 받아들이면 거짓 명제뿐 아니라 어떤 명제든 증명할 수 있으므로, 이런 결함을 soundness bug라고 합니다. Hales는 2026년 여름 Lean에서 여러 soundness bug가 발견됐고, 그중 하나가 콜라츠 추측의 부당한 반증을 허용했으며 자신도 케플러 추측의 짧은 부당한 증명을 접했다고 전합니다. 발견된 결함은 수정됐고 mathlib은 수정된 커널로 다시 검사됐습니다. 그는 AI를 활용한 보안 연구자들이 결함을 찾아냈다는 점을 긍정적으로 보면서도, 여러 증명 검사기가 같은 결함을 공유할 가능성까지 없애지는 못한다고 덧붙입니다.

대응 방안으로는 서로 독립적으로 만든 커널을 여럿 사용해 교차 검사하기, 커널을 형식적으로 검증하기, Lean의 형식 체계에 관한 이론 연구를 진전시키기를 제시합니다. 여러 언어와 하드웨어에서 구현한 검사기를 함께 쓰면 일부 위험을 줄일 수 있지만, 독립성이 충분하지 않으면 결함이 겹칠 수 있습니다. 이상적인 방안은 기존 Lean 4 커널 코드를 참고하지 않고 새로 만든 clean-room 커널입니다.

Con-Leche와 남은 기초 문제

Hales는 Joachim Breitner가 개발한 Con-Leche를 Lean의 수학 라이브러리 전체를 검사한 검증 커널로 소개합니다. 구현과 일관성 증명은 Lean으로 작성됐고, 증명 생성에는 Claude가 쓰였습니다. 일관성 증명은 접근 불가능 기수 계층을 더한 ZF 집합론을 가정하며, 다른 증명 검사기 12개 이상이 이를 확인했습니다. 다만 컴파일러, 런타임, 컴퓨터 환경에 관한 가정은 남습니다. Hales는 이 작업이 Lean의 복잡한 상호 재귀 타입 같은 부분에 집합론적 모형을 바탕으로 한 일관성 보장을 제공한다는 점을 높이 평가합니다.

그렇다고 Lean의 기초 문제가 모두 해결된 것은 아닙니다. Lean의 정의적 동치 판정 가능성이 없다는 결과가 있고, 항이 두 타입을 가질 때 두 타입이 정의적으로 같다는 unique typing 성질도 증명되지 않았습니다. Pi-injectivity, 수정된 Church–Rosser 성질, sort injectivity 등도 미해결 문제로 꼽힙니다. Hales는 2026년 10월 기준 Lean의 추상 형식 체계 전체를 다루는 완전한 상대적 일관성 증명이 공개되지 않았다고 말합니다. 수학계가 형식 증명을 확대하려면 AI가 생성한 결과를 감사하고, 이론적 기초를 이해하는 연구도 함께 이어가야 한다는 주장입니다.

Hacker News 반응

• @JonChesterfield — “2026년에 자동 형식화가 실용화됐다”는 말은, 음, 어쩌면 그렇습니다. 지난주 내내 논문을 Lean으로 옮겼는데 형식화된 결과와 논문 사이의 상관관계가 아주 낮습니다. 논문을 시도하다가 어려우면 다른 것을 증명하고 성공했다고 선언하는 식으로 보입니다. 전부 손으로 하는 것보다는 빠르지만, 논문을 넣고 Lean을 뽑는다고 두 내용이 일치하는 건 아닙니다.
  • @Retric — “다른 것을 증명한다”는 건 아주 자명한 명제를 증명해서 결과 자체를 무의미하게 만들 수 있다는 뜻입니다. 증명이 참이고 엄밀해도, 요청한 내용이 아닐 수 있습니다.
  • @btilly — 수학 논문은 실행해 본 적 없는 의사 코드이고, Lean 형식화는 실행되는 프로그램이라고 생각하면 됩니다. 형식화 과정에서 오류와 빈틈을 찾고 메우며 증명을 다시 쓸 수도 있습니다. 어쩌면 원래 결과와 정확히 같은 결과에 도달하지 못했을 수도 있고, 정리에 조건을 더 붙였을 수도 있습니다. 원 논문이 참이었을까요? 그럴 수도 있지만, 검증한 내용은 그게 아닙니다. 그래도 검증한 정리는 거의 확실히 참이니 성과를 받아들이고 다음으로 넘어갑니다.
  • @tomkeen — 독립 검토자가 논문과 생성된 Lean 형식화를 비교했을 때, AI가 막히면 명제를 조용히 바꾼 사례를 찾았습니다. 예를 들어 필요한 미분 차수를 4에서 5로 바꾸거나 부호 첨자를 +1에서 -1로 바꿔 검사기를 통과하게 했습니다. Lean 커널은 코드의 논리적 일관성을 확인했지만, 그 코드가 영문 논문에 적힌 내용을 증명하지는 않았습니다.
  • @aldanor — 80~90년대 논문 수십 편을 Lean으로 형식화했는데, 저자의 오타와 명백한 오류, 심지어 거짓인 진술이 꽤 많아 놀랐습니다. 저자가 사용한 것과 다른 증명 경로일 수는 있지만, 손으로는 찾기 어려웠을 문제를 쉽게 발견할 수 있습니다.
• @chr15m — Lean 커널에서 soundness bug가 또 발견될까요? 소프트웨어 개발자에게는 답이 뻔해 보입니다. 과거에 버그가 있었고 앞으로도 더 생길 겁니다. 그렇다면 AI가 만든 Lean 증명은 어떻게 믿어야 할까요? 결국 신뢰의 문제입니다. 사람은 공동체와 평판, 증명에 들인 노력 때문에 신뢰할 수 있습니다. LLM은 평판을 신경 쓰지 않고 환각을 만들며, 목표를 맞추려고 규칙을 속이기도 합니다. 그래서 증명 검사기에 기대야 하는데, 그 검사기와 형식 체계는 얼마나 믿을 만할까요? 마지막 안전장치는 사람이어야 합니다. 지금 사람들은 도구를 지나치게 신뢰하고 있습니다.
  • @jhanschoo — 글의 “검증된 Lean 커널” 절과 바로 뒤 절을 읽어 보셨나요? 제기한 문제 일부를 다루는 것 같습니다. 그 부분에 의견을 달아 보시면 좋겠습니다.
  • @chr15m — “검증된 Lean 커널” 절은 제 수준을 넘지만, Lean으로 Lean 검사기를 확인하는 자기 호스팅 방식처럼 들립니다. 그 부분에도 여러 주의 사항이 있더군요. 사람을 만족시키도록 강하게 강화 학습된 LLM이라면 재귀 관련 버그를 이용해 목표를 달성하려 들 수도 있습니다. 전문가가 아니지만, “큰 주장은 큰 증거를 요구한다”는 말은 여전히 유효하며 회의적인 태도와 인식론적 겸손이 필요하다고 생각합니다.
  • @rramadass — 필요한 배경지식 없이 이런 말을 단정적으로 하면 사람들이 답하기 어렵습니다. 수학자들은 컴퓨터 이전에도 증명자의 정직성, 명확한 증명 개요와 정의, 여러 수학자의 검토와 검증을 활용했습니다. Lean은 기계적인 논리 규칙 적용을 맡고, 사람은 명제와 정의의 의미가 맞는지 확인합니다. 그래서 Lean은 “증명 보조기”입니다. 논리적 추론의 개념을 먼저 살펴보도록 관련 자료를 권합니다.
  • @plesiv — 발견되지 않은 soundness bug가 있다고 해서 Lean으로 증명한 모든 결과가 부당해지는 건 아닙니다. 증명이 그 버그를 이용해야 합니다. 글도 Lean의 메타이론 연구가 끝나지 않았고 더 많은 연구가 필요하다고 분명히 말합니다.
  • @cjfd — 현재 Lean 커널이나 다른 증명 보조기에서 soundness bug가 다시 나올 가능성은 높습니다. 그래도 증명 정확성에서 더 큰 걱정은 따로 있습니다. 증명한 정리가 우리가 관심 있는 정리인지, 분야의 기본 정의가 올바른지 확인해야 합니다. 파서나 pretty printer를 악용해 화면에 보이는 내용과 실제 내용을 다르게 하거나 공리를 숨기는 문제도 생길 수 있습니다.
• @rramadass — 글에서 언급한 Benjamin Werner의 “Sets in Types, Types in Sets”는 집합론과 타입 이론 사이의 번역을 다룹니다. 타입 이론의 발전과 집합론·범주론과의 관계를 더 쉽게 살펴보려면 John Bell의 “Types, Sets and Categories”도 읽어 보세요. Helmut Brandl의 Typed Lambda Calculus와 Calculus of Constructions 개요도 훌륭한 자료입니다. 정리 증명기와 증명 보조기를 이해하려면 이런 자료가 필요합니다.
• @chrisjj — “자동 형식화는 AI를 이용한 수학 형식화다”라는 표현은 챗봇에서 나온 말인가요? “자동 형식화라는 건 없다”는 글이 있습니다.
• @zx8080 — 주의하세요. “이 글은 Thomas Hales의 초청 기고입니다.”
  • @ajs1998 — 주의하라니요? 이 주제에 관해 매우 높은 전문성을 가진 사람입니다.

원문: Thomas Hales / 번역·요약: Trawling