수학자들이 리안(Lean) 정리 증명기에 대해 알아야 할 것: 신뢰성과 AI

이 글은 Thomas Hales의 기고문입니다. 이 블로그 게시물은 원래 다른 파일 형식으로 작성되었으며 AI를 사용하여 변환되었습니다. — T.

수학자들은 수학에서 무엇을 가치 있게 여기는지에 대해 논해 왔습니다. 저에게 중요한 것은 수학의 일관성과 과학 및 문명을 뒷받침하는 그 비할 데 없는 신뢰성입니다.

수학의 형식화(Formalization of Math)

형식 증명(formal proof)이란 수학적 증명이 수학의 기초와 논리의 근본 규칙 수준에서 철저하게 검증된 것을 의미합니다. 이론적으로는 손으로 할 수도 있지만, 관련된 단계의 수가 많기 때문에 일반적으로 이 작업에 맞춰 설계된 소프트웨어를 사용하여 컴퓨터로 수행됩니다.

형식화가 이루어진 정리들의 예로는 네 가지 색 정리(four-color theorem), Feit-Thompson (홀수 차수) 정리(odd-order theorem), 케플러 추측(Kepler conjecture), 구 전개(sphere eversion), 8차원 및 24차원의 구 채우기 문제(sphere packing problem), 나비에-스토크스 강제 블로우업(Navier-Stokes forced blowup), 그리고 페르마의 마지막 정리(Fermat’s Last Theorem) 등이 있습니다. 이 중 마지막 세 가지 형식화 프로젝트는 올해 완료되었으며, 형식화의 잠재력에 대한 광범위한 인식을 가져왔습니다.

형식화를 위한 소프트웨어 시스템은 증명 보조기(proof assistants), 정리 증명기(theorem provers), 또는 대화형 정리 증명기(interactive theorem provers) 등으로 다양하게 불립니다. 이 게시물의 목적을 위해, 이 용어들은 상호 교환적으로 사용됩니다. 수년 동안 많은 증명 보조기들이 개발되었습니다: Automath, HOL Light, Isabelle, Coq (작년에 Rocq으로 이름이 변경됨), Metamath, Mizar, 그리고 Lean. Freek Wiedijk는 일부 증명 보조기를 비교하는 책

Lean은 2013년 Microsoft 재직 중 Leo de Moura에 의해 개발되어 소개되었습니다. 저희에게 큰 도움이 된 것은 de Moura가 Microsoft를 설득하여 이 소프트웨어를 오픈 소스로 만들게 한 것입니다. Kevin Hartnett의 Lean 역사 관련 서적, “The Proof in the Code”에 따르면 Jeremy Avigad(카네기 멜런의 새로운 NSF 연구소 ICARM 책임자)가 Lean의 최초 사용자였습니다. 그는 2015년에 Lean 세미나를 열었고 제가 참석했습니다. 2017년에는 Jeremy의 대학원생 중 한 명인 Mario Carneiro가 Johannes Hölzl과 협력하여 기존 Lean 코어 라이브러리의 일부를 가져와 mathlib이라는 별도의 Lean 수학 라이브러리를 시작했습니다. 이 형식화된 수학 라이브러리는 현재 방대하며, 약 30만 개의 정리(theorem), 10만 개 이상의 정의(definition), 250만 줄의 코드, 그리고 700명이 넘는 기여자들을 포함하고 있습니다. mathlib의 모든 정의나 정리는 추가적인 정리를 증명하는 데 사용될 수 있습니다. 예를 들어, 어떤 증명이 코시-슈바르츠 부등식(Cauchy-Schwarz inequality)을 사용한다면, 이를 다시 증명할 필요 없이 라이브러리에서 인용하여 결과를 사용할 수 있습니다.

자동 형식화는 실질적인 현실입니다 (Autoformalization is a practical reality)

과거에는 연구자들이 논문 형태의 증명을 인간의 노동력으로 형식적 증명(formal proof)으로 옮겨야 했습니다. 예를 들어, 3차원 구 배열에 대한 케플러 추측(Kepler conjecture)의 형식적 증명은 완료하는 데 약 20년의 인력 투입이 필요했으며, 약 50만 줄의 증명 스크립트로 구성되어 있습니다. 수년간, 형식화 분야에서 일하는 우리 중 많은 사람들에게 이 과정에 자동화를 늘릴 방법을 찾는 것이 꿈이었습니다. 자동 형식화(Autoformalization)는 그 꿈의 실현입니다. 자동 형식화란 AI를 통해 수학을 형식화하는 것입니다. AI가 논문(예: pdf 또는 tex 파일)을 읽고 Lean이나 다른 증명 보조 도구에서 형식적 증명을 출력합니다.

자동 형식화는 2026년에 실질적인 현실이 되었습니다. 2025년 후반 봄과 여름부터 연구자들은 자동 형식화에 대해 점점 더 낙관적이게 되었습니다. 다음은 몇 가지 주요 이정표입니다.

• 2025년 9월, Math Inc.는 소수 정리(prime number theorem)의 준자동 형식화(quasi-autoformalization)를 발표했습니다. 이 과정은 AI가 막힐 때마다 인간이 추가적인 지침을 제공해야 했기 때문에 단순히 “준(quasi)”에 그쳤습니다.
• 2026년 1월, J. Urban은 set theory 기반의 증명 보조 도구에서 Munkres의 위상수학 교과서 대규모 부분을 형식화한 아카이브 프리프린트(“130k lines of formal topology in two weeks”)를 게시했습니다.
• 2026년 3월. 8차원에서 형식화 완료를 발표한 지 약 일주일 만에, Math Inc.는 Viazovska와 그녀의 협력자들이 증명한 것을 따라 24차원 구형 패킹 문제(sphere-packing problem)의 자동 형식화(autoformalization)를 발표했습니다. 이 프로젝트는 약 500K SLOC (source lines of code)를 생성했으며, 이후 골핑(golfing, 코드 간소화)을 통해 약 200K 라인으로 줄어들었습니다.
• 2026년 5월, Meta/Facebook Research의 한 그룹은 ATLAS라는 프로젝트에서 26개의 수학 교과서 대규모 부분을 자동 형식화했습니다.

이후 수많은 정리들이 자동 형식화되었습니다. 특히 주목할 만한 것은 Anthropic이 9월 4일에 발표한 페르마의 마지막 정리(Fermat’s Last Theorem)의 자동 형식화입니다. 이 프로젝트는 11일 동안 Lean 언어로 1,300만 라인의 코드를 생성했습니다. OpenAI가 9월 8일에 강제력을 가진 나비에-스토크스 폭발(Navier-Stokes blowup with forcing)을 발표했을 때는 해당 정리의 Lean 자동 형식화도 함께 공개되었습니다.

앞으로를 내다보며 Urban은 1월에 “어떤 증명 보조 도구를 사용하든 관계없이, (자동) 형식화가 2026년에는 상당히 쉽고 어디서나 흔하게 될 것이라고 믿습니다”라고 말했습니다. 자동 형식화 프로젝트는 다양한 LLM을 사용하여 여러 증명 보조 도구에서 완료되었지만, 우리는 Lean에 초점을 맞추고 있습니다. “[Jesse] Han에게 이것은 더 큰 의미를 지닙니다: 극도로 대규모의 형식화가 일상적인 수학 혁명적 변화의 시작점입니다”(IEEE Spectrum). Jared Lichtman은 2026년 9월 8일에 'MAP (Mathematics Autoformalization Project)' 출범을 발표했습니다. 이 프로젝트는 “알려진 모든 수학을 형식 코드로 번역”하는 것을 목표로 합니다. 그는 우리에게 다음 1조 라인의 코드를 상상해 보라고 요청합니다.

Lean은 신뢰할 수 있을까?

타입 이론(Type theory)

Lean은 타입 이론에 기반을 두고 있으며, 실제로 '귀납적 구성의 계산(calculus of inductive constructions)'이라고 불리는 CIC라는 특정 방언의 타입 이론입니다. 이 글은 타입 이론에 대한 튜토리얼이 아니므로 간략하게 다루겠습니다. 1901년 러셀(Russell)의 유명한 역설(자기 자신이 원소가 아닌 모든 집합들의 집합….)은 수학 기초론에 위기를 초래했습니다. 그 해에 두 가지 해결책이 제안되었습니다. (1) 안전하지 않은 집합의 생성을 금지하는 체르멜로(Zermelo)의 집합론 공리계; (2) 러셀 역설과 같은 실체를 생성하는 것이 구문 오류(syntax error)가 되도록 만드는 타입 이론입니다. 타입 이론은 1903년 러셀 자신이 저서 『수학 원리(Principles of Mathematics)』에서 도입했으며, 러셀과 화이트헤드의 『프린키피아(Principia)』의 기초 시스템 일부가 되었습니다.

집합론에 익숙한 수학자들에게는 B. Werner의 논문 (1997년) "타입 속의 집합, 집합 속의 타입(Sets in Types, Types in Sets)"이 어떤 내용을 하든 타입 이론으로 번역될 수 있으며, 타입 이론에서 무엇을 하든 다시 집합론으로 번역될 수 있다는 안심을 줍니다. 더 정확히 말하자면, 이 논문은 ZFC 집합론이 CIC로 인코딩될 수 있고, CIC의 특정 방언이 ZFC(접근 불가능한 기수 계층 구조가 추가된)로 다시 인코딩될 수 있음을 보여줍니다.

상황을 지나치게 단순화할 위험을 감수하자면, "타입은 서로소인 집합과 같다"고 말할 수 있습니다. 타입 이론의 각 원소는 정확히 하나의 타입에 속합니다. 자연수 2의 타입은 자연수 타입을 이루며, 자연로그의 밑 $e$의 타입은 실수 타입을 이루고, 그 외에도 마찬가지입니다. 자연수의 타입은 실수 타입과 서로소이며, 명시적 강제 변환(coercion) (2를 2.0으로 보내는 것)이 자연수 타입에서 실수 타입으로 구성됩니다. 제가 강의할 때, 가끔 집합을 공집합 교차 부분이 없는 벤 다이어그램으로 그리고, 타입을 서로 간에 교차하지 않고 쌓아 올린 벽돌 무더기로 비유합니다.

Lean의 설계

Lean 시스템의 한 부분은 범용 프로그래밍 언어(적절하게는 Lean 프로그래밍 언어라고 불림)입니다. 목록을 정렬하는 프로그램과 같은 일반적인 컴퓨터 프로그램은 이 언어로 작성될 수 있으며, 이후 컴파일되어 실행됩니다. Lean 시스템은 또한 정의를 작성하고, 정리(theorem)를 진술하며, 증명 스크립트를 작성할 수 있는 수학적 언어를 제공합니다. 프로그래밍 언어와 수학적 언어는 독립적인 개체가 아닙니다. 오히려 둘 다 수행하는 단일 언어입니다. 프로그램 코드는 알고리즘의 정확성에 대한 정리와 혼합될 수 있으며; 수학적 증명은 프로그램을 사용하여 생성될 수 있습니다. Lean의 증명 스크립트는 파싱(parsed)되어 엘라보레이션(elaboration, 일종의 수학 컴파일 과정)이라는 과정을 거친 후, Lean 커널에 의해 검사됩니다. 커널의 책임은 엘라보레이션의 출력을 확인하고 검증하는 것입니다.

Lean 커널은 수천 줄의 C++ 코드로 이루어져 있습니다. 이 커널은 신중하게 설계되었지만 극도로 복잡합니다. 위에서 언급했듯이, mathlib은 Lean 언어로 작성된 약 250만 SLOC(Source Lines of Code)로 구성되어 있습니다. 이 라이브러리는 엘라보레이션된 후, 커널에 의해 검사됩니다. 만약 이 250만 줄의 코드 어딘가에 무조건적인 거짓 증명이 존재한다면, 그것은 거짓 증명을 거부하지 못한 커널 또는 런타임의 결함입니다. 근본적인 타입 이론(type theory)의 모든 결함은 코드로 구현된 경우 심각한 커널 결함이 됩니다.

Lean 증명은 커널에 의해 검사되기 전까지는 믿어서는 안 됩니다. 또한, Lean의 증명은 진술 충실성(statement fidelity)을 보장하기 위해 인간의 감사가 수행될 때까지 받아들여져서는 안 됩니다. 검증된 정리가 우리가 생각하는 것과 같은가? Lean에 있는 정의들이 우리가 그래야 한다고 생각하는 것에 부합하는가? 이 작업은 일반적으로 증명 자체를 확인하는 것보다 훨씬 쉽습니다. 예를 들어, Navier-Stokes의 경우, 인간은 Lean에 있는 진술이 Fefferman이 제시한 밀레니엄 문제(Millennium Prize Problem)의 진술과 일치하는지, 그리고 특히 실수 체(field of real numbers), 편미분(partial derivatives), 측도(measure)와 같은 개념들이 Lean에서 올바르게 정의되었는지 확인해야 합니다. Lean의 비교 도구(comparator tool)가 이 작업에 도움을 줍니다. 이 도구는 또한 가능한 무단 공리(unauthorized axioms) 검사 등 추가적인 점검을 수행할 수 있습니다.

건전성 버그의 여름 (Summer of Soundness Bugs)

건전성 버그(soundness bug)란 '거짓(False)'의 증명을 허용하여 결과적으로 모든 명제(any proposition)의 증명을 가능하게 하는 커널 내의 결함입니다. 건전성 버그는 증명 보조기(proof assistant)에서 발생할 수 있는 가장 파괴적인 종류의 버그이며, 수학적 신뢰성에 깊이 관심을 가진 수학자들에게 경고를 울려야 합니다. 때때로 다양한 증명 보조기에서 건전성 버그가 발견됩니다. 2003년, 저는 당시 모든 커널 중 가장 신뢰성이 높은 것으로 간주되었던 증명 보조기 HOL Light에서 건전성 버그를 발견했습니다. 그 커널은 몇 백 줄의 컴퓨터 코드로만 구성되어 있습니다. 저에게는 1996년 이후 이 증명 보조기에서 발견된 첫 번째 건전성 버그였던 것을 제가 찾아냈다는 것이 영광스러운 배지(badge of honor)와 같습니다. (HOL Light 변경 로그, 2003년 7월 참조.)

Lean 4는 2023년 9월에 출시되었습니다. 출시 이전에 두 개의 건전성 버그(soundness bugs)가 발견되어 수정되었습니다. 2025년 5월에는 오버플로우로 인해 또 다른 건전성 버그가 보고되었고, 2026년 봄과 여름에는 “건전성 버그의 여름(Summer of Soundness Bugs)”이라 불리는 대혼란이 벌어졌습니다. 7월과 8월에 걸쳐 Lean에서 여러 개의 건전성 버그가 발견되었습니다. 이 여름철 혼란은 다양한 증명 보조기(proof assistants)에 영향을 미쳤지만, 저는 Lean에 초점을 맞추었습니다. 하나의 Lean 버그는 Collatz 추측에 대한 부적절한 반증을 야기했습니다. 저는 올여름, 이 버그가 Lean에서 Kepler 추측의 짧은 부적절한 증명을 생성했을 때 이를 알게 되었습니다. 이러한 모든 버그들은 신속하게 수리되었고, mathlib는 수정된 커널에 의해 검증되었습니다. 건전성 버그에 대한 분석은 de Moura의 사후 보고서(postmortem)에서 찾아볼 수 있습니다.

“Lean 건전성 버그의 여름”은 재앙처럼 들릴 수 있지만, 더 깊이 조사해 보면 이러한 건전성 버그의 발견 자체가 긍정적인 발전임을 알 수 있습니다. 이 여름철 버그들은 블랙햇 해커에 의해서가 아니라, 신뢰할 수 있는 커널(reliable kernels)에 관심 있는 보안 연구원들이 보유한 최첨단 모델 AI(frontier model AI)에 의해 감지되었습니다. Collatz 버그는 “CakeML: ML의 검증된 구현체”를 공동 작성한 Ramana Kumar가 발견했습니다. CakeML은 종단 간(end-to-end) 검증된 ML(함수형 프로그래밍 언어)을 생성합니다. 여러 개의 버그는 Dan Selsam에 의해 발견되었습니다. de Moura의 보고서에 따르면, “OpenAI의 Daniel Selsam이 사이버 보안 전문 AI를 갖춘 Lean FRO를 지원하여 Lean 커널에서 다른 프로그래밍 실수들을 찾아냈습니다. 이 모든 것들은 수정되었습니다.” Selsam과의 협업은 “내부 AI가 추가적인 문제를 찾을 수 없다고 보고했을 때” 종료되었습니다. Dan Selsam은 Lean의 초기 시절부터 기여해 왔으며, Lean으로 검증되는 IMO 수준의 문제 해결을 목표로 하는 IMO 그랜드 챌린지(IMO grand challenge)의 창시자 중 한 명이었습니다. 그는 최근 X.com에 올라온 바이럴 게시물에서 AI 안전성에 대한 경고를 하면서 언론의 주목을 받았습니다.