왜 그냥 Lean만 쓰지 않나요?

4 hours ago 2

수학 형식화의 역사는 Lean으로 시작되지 않았고, 거의 60년 전부터 여러 계보의 시스템이 핵심 기법과 성과를 이미 축적해 옴
1968년의 AUTOMATH, LCF 계열, HOL, Rocq, ACL2, Mizar 같은 도구들은 실해석학부터 소수 정리, 네 가지 색 정리, Kepler 추측까지 폭넓은 형식화를 이뤄 냄
Lean은 큰 라이브러리와 활발한 공동체를 바탕으로 현대 수학 정의를 빠르게 쌓아 올렸지만, propositions as types나 의존 타입이 proof assistant의 유일한 길은 아님
Isabelle은 강한 자동화, 높은 가독성, 의존 타입 회피를 장점으로 내세우며, proof object 없이도 커널의 추상화 장벽으로 증명 검사를 구성하는 LCF 전통을 잇고 있음
AI가 구조화된 증명을 정리하고 다른 시스템으로 번역하는 흐름까지 더해지면서, 한 도구만 절대적 기준으로 보는 부담은 앞으로 더 줄어들 수 있음

초기 시스템과 다른 계보들

AUTOMATH
- AUTOMATH는 1968년에 이미 수학 형식화에 필요한 요소 대부분을 포함했음
- 1977년 Jutting은 AUTOMATH로 Landau의 Foundations of Analysis를 형식화했고, 순수 논리에서 출발해 복소수 구성까지 다룸
- 동치류와 유리수 집합을 사용했고, 실수선의 Dedekind 완비성도 형식적으로 증명함
- 이 성과는 20년 동안 다시 나오지 않았고, 1990년대 중반에야 John Harrison의 HOL Light와 Jacques Fleuriot의 Isabelle/HOL에서 다시 실수 형식화가 이뤄짐
- 표기법은 매우 불편했고 자동화도 전혀 없어 증명이 길고 읽기 어려웠음
- 그럼에도 동치류를 다루는 데서는 Rocq보다 낫다고 보며, Rocq 사용자들이 겪는 setoid hell과 달리 Jutting은 동치류 형식화를 차분하게 수행함
Boyer와 Moore
- Robert Boyer, J Moore 계열의 computational logic은 수학이 아니라 코드 검증을 목표로 출발함
- 1973년 논문 Proving theorems about LISP functions에서 이 방향이 처음 드러남
- 일반 수학에는 분명한 한계가 있었지만, Gödel의 불완전성 정리, quadratic reciprocity, Banach–Tarski 정리 같은 깊은 결과의 형식화에도 쓰였음
- 현재 계보인 ACL2는 주로 하드웨어 검증에 적용됨

LCF 이후의 흐름

Edinburgh LCF는 프로그래밍 언어 이론에 집중했지만, 증명 도우미의 메타언어로 함수형 언어를 두는 발상은 널리 퍼짐
Cambridge, INRIA, Cornell 등 여러 그룹이 ML을 사용해 초기 HOL, Coq(현 Rocq), Nuprl 같은 도구를 만듦
HOL 그룹은 하드웨어 검증에 집중했지만, 부동소수점 하드웨어 검증 때문에 실해석학이 필요해졌음
John Harrison은 Cauchy 적분 공식을 통해 소수 정리 같은 본격적인 수학 결과를 HOL 계열에서 증명함
100 theorems를 가능한 많이 검증하려는 목표 아래 HOL Light는 자주 최상위권에 올랐음
2014년까지 이 계열 시스템들은 여러 고급 정리를 형식화했음
- 네 가지 색 정리
- odd order theorem
- 선택 공리의 상대적 무모순성
- Gödel의 두 번째 불완전성 정리
- Tom Hales의 Kepler 추측
이 정리들은 대체로 증명이 길고 복잡했고, 형식화 작업도 매우 큰 규모였으며, 정리에 남아 있던 의문을 줄이는 데 핵심 역할을 함

Lean 공동체의 부상

수학자들은 앞선 형식화 성과들이 Grothendieck schemes나 perfectoid spaces 같은 주류 현대수학의 정교한 구성까지는 다루지 못했다고 봤음
Tom Hales는 이런 정의들을 라이브러리로 쌓아 올리는 방향을 택했고, 증명보다 정의의 축적에 초점을 두며 Lean을 선택함
그는 Big Proof 프로그램에서 이 방향을 발표했고, 비슷한 구상도 함께 논의됨
Kevin Buzzard가 이를 듣고 교육에 Lean을 써보기로 하면서 이후 확산이 빨라짐
Lean 공동체의 중요한 전환점으로, Rocq를 오래 지배한 구성적 증명 집착에서 벗어난 점이 제시됨
직관주의는 Russell의 역설 이후 등장했고, 실수 개념에도 특정한 함의를 가졌음
Martin-Löf type theory는 분명히 직관주의적 형식주의이지만 Rocq는 그렇게 단순하게 볼 수 없다고 적음
그럼에도 Rocq 관련 논문들에서는 구성적 증명이 무관하거나 무의미한 자리에서도 반복적으로 등장했고, 이런 경향이 Rocq의 수학 적용을 가로막으면서 자리를 Lean에 넘겨줬다고 봄

propositions as types와 LCF의 차이

Propositions as types는 논리 기호 ∀, ∃, →, ∧, ∨ 와 타입 생성자 Π, Σ, →, ×, + 를 연결하는 이중성임
이 틀은 아름답고 이론적으로 생산적이지만 유일한 길은 아님
proof assistant를 propositions as types 원리로 증명을 검사하는 소프트웨어로 한정하면, 지난 반세기 연구의 대부분이 정의 밖으로 밀려남
그렇게 되면 Rocq, Lean, Agda만 남게 됨
AUTOMATH조차 propositions as types의 사례는 아니며, Π와 → 비슷한 요소는 있어도 논리는 일반 논리 교재처럼 공리들로 설정함
de Bruijn은 50년 전에 이미 타입과 명제의 분리가 필요하다고 봤음
대표적으로 나눗셈은 세 인자를 받아야 하고, (x/y)의 값은 (y \ne 0)의 증명에 의존하게 되므로 proof irrelevance가 필요하다고 적음
LCF 접근이 propositions as types와 같다는 인식도 사실과 다르다고 못박음
- LCF 관련 글
Rocq와 Lean에는 명제의 sort인 Prop가 있으며, 여기서는 같은 명제의 모든 증명 객체가 같은 값으로 평가돼 proof irrelevance를 제공함
그렇다고 거대한 증명 객체가 사라지는 것은 아니며 실제 시스템에는 여전히 남아 있음
Robin Milner의 핵심 발견은 LCF에서 증명 객체 자체가 필요 없다는 점이었음
ML의 추상 데이터 타입 안에 증명 커널을 넣고, 추론 규칙을 생성자로 두면 동적으로 증명을 검사할 수 있음
ML의 abstraction barrier 덕분에 부정행위가 불가능하다고 봄
거대한 항이 아무것도 지시하지 않는데도 수십 MB를 차지하는 일은 RAMmageddon 시대에 특히 비합리적으로 다가옴
그런 불필요한 항을 더 우아하게 만드는 연구까지 이어지는 점도 비판함

Isabelle을 고를 이유

동료들이 Lean을 쓰고, 팀의 전문성도 Lean에 있고, 필요한 전제 라이브러리도 Lean에 있다면 Lean을 쓰는 편이 자연스러움
다만 자유롭게 선택할 수 있다면 Isabelle을 검토할 이유는 분명함
자동화
- 가장 강력한 자동화를 장점으로 들며, 일상적인 “hammer”들과 비교해도 sledgehammer에 견줄 것은 없다고 평가함
- 컴퓨터 대수 쪽도 별도로 다룰 필요가 있다고 적음
가독성
- 가독성 면에서 최선의 선택지로 두며, Isar 관련 예시들을 근거로 듦
의존 타입 회피
- 의존 타입이 없기 때문에 universe level과 초보자를 곤란하게 만드는 여러 특이점을 피할 수 있음
- Lean의 mathlib와 Rocq의 SSReflect, Mathematical Components에서도 의존 타입 사용은 권장되지 않는다고 적음
- 의존 타입의 핵심 난점은 제대로 구현하면 타입 검사 자체가 결정 불가능해진다는 점임
- 이는 동등성 판정이 결정 불가능하기 때문이며, 초기에는 이 점이 당연하게 받아들여졌다고 적음
- 1990년 무렵부터는 타입 검사를 결정 가능하게 만들기 위해 동등성을 definitional/intensional equality로 낮추는 쪽으로 합의가 이동함
- 그 결과 (T(N+1))과 (T(1+N))은 서로 다른 타입이 됨
- 이런 제한은 실제 증명에도 영향을 주며, definitional equality 검사 자체도 여전히 계산 부담이 큼