| source | https://lawrencecpaulson.github.io//2026/04/23/Why_not_Lean.html |
|---|---|
| created | 2026-04-30 |
| by | openai:gpt-5.4 |
[ 오토매스(AUTOMATH) LCF HOL 시스템(HOL system) HOL 라이트(HOL Light) 린(Lean) 형식화된 수학(formalised mathematics) ]
요즘 수학을 형식화하자고 제안하면, 왜 린(Lean)을 쓰지 않는지 설명해야 한다는 말을 들었다. 그러면 내가 40년 전에 왜 종속형(dependent type)의 세계를 떠났는지 다시 떠올리게 된다. 그 세계의 교조성, 폐쇄성, 동조 압력 때문이다. 린은 훌륭한 언어다. 도구도 좋고, 라이브러리도 크며, 거대하고 열정적인 사용자 공동체도 있다. 최근에는 놀라운 성과도 잇달아 냈다. 그러나 수학의 형식화 역사가 거의 60년에 이른다는 사실을 잊어서는 안 된다. 오늘날의 진전을 둘러싼 과열된 분위기 속에서도, 우리가 어떻게 여기까지 왔는지는 기억해야 한다. 군중을 따라간 사람들이 이끌어 온 길은 아니었다.
위에서 말한 과열된 분위기의 일부는 “린이 수학의 형식화를 가능하게 만들었다”는 주장으로 자주 드러난다. 미안하지만, 우리는 이미 1968년에 거기 도달했다. N. G. 더브라위너르의 오토매스(AUTOMATH)에는 이미 필요한 요소가 거의 다 들어 있었다. 1977년에는 유팅(Jutting)이 이를 이용해 란다우의 해석학의 기초(Foundations of Analysis) 를 형식화했다. 이 책은 순수 논리에서 출발해 복소수 체계를 구성하는 내용을 담고 있다. 유팅은 동치류(equivalence class)와 유리수 집합을 다뤘다. 그는 실수 직선의 데데킨트 완비성(Dedekind completeness)도 형식적으로 증명했다. 이 성과는 이후 컴퓨터 성능이 엄청나게 발전했는데도 20년 동안 다시 나오지 못했다. 마침내 1990년대 중반이 되어서야 존 해리슨(John Harrison)이 HOL 라이트를 이용해, 자크 플뢰리오(Jacques Fleuriot)가 이자벨/HOL을 이용해 실수를 다시 형식화했다.
내 생각에, 오늘날 어떤 시스템에서 형식화된 것이든 거의 모두 오토매스에서도 형식화할 수 있었을 것이다. 주요 약점은 표기법이었다. 정말 끔찍했다. 자동화도 전혀 없었다. 그래서 증명은 길고 읽기 어려웠다.
그런데도 동치류를 다루는 데에는 지금도 아마 로크(Rocq)보다 낫다. 후자의 사용자들은 “세토이드 지옥(setoid hell)”을 두고 불평하지만, 유팅은 자신의 학위 논문에서 동치류 형식화를 담담하게 서술한다. 그는 란다우의 한 장을 아예 두 번째로 다시 형식화하기도 했다. 자신이 보기에 올바른 접근이 동치류였기 때문이다.
완전히 다른 계통에서는 로버트 보이어(Robert Boyer), J 무어(J Moore)와 많은 동료들의 연구가 나왔다. 그들의 작업은 1973년에 “LISP 함수에 관한 정리 증명(Proving theorems about LISP functions)”이라는 제목으로 처음 발표됐다. 그들이 내세운 목표는 수학이 아니라 코드 검증이었다. 그들의 “계산 논리(computational logic)”는 일반 수학에는 분명한 한계가 있다. 하지만 그렇다고 해서 깊이 있는 여러 결과를 형식화하는 데 쓰이지 못한 것은 아니다. 괴델의 불완전성 정리(Gödel’s incompleteness theorem), 이차 상호법칙(quadratic reciprocity), 바나흐–타르스키 정리(Banach–Tarski theorem)에 이르기까지 다양한 결과가 거기서 나왔다. 현재 이 계열의 구현은 ACL2라고 하며, 주로 하드웨어 검증에 쓰인다. 남들과 다르게 가도 멀리 갈 수 있다.
획기적이었던 에든버러 LCF(Edinburgh LCF)는 프로그래밍 언어 이론에 좁게 초점을 맞췄다. 그러나 증명 보조기의 메타언어(metalanguage) 로 함수형 프로그래밍 언어를 두자는 발상, 그래서 ML이라는 이름이 붙은 그 아이디어는 폭넓은 영향을 남겼다. 케임브리지, INRIA, 코넬과 그 밖의 여러 집단은 ML을 이용해 도구를 만들었고, 그 안에는 HOL, 코크(현재의 로크), 누프를(Nuprl)의 초기 버전도 있었다. HOL 그룹은 하드웨어 검증에 강하게 매달려 있었지만, 부동소수점 하드웨어를 검증하려면 실해석이 필요했다. 곧 존 해리슨은 코시의 적분 공식(Cauchy’s integral formula)을 통한 소수정리 같은 본격적인 수학을 증명했다. 그는 유명한 100개의 정리(100 theorems) 를 가능한 한 많이 검증하겠다는 과제를 스스로에게 부여했고, HOL 라이트는 종종 그 순위표 맨 위에 오른다. 이자벨이 때로 HOL 라이트를 앞선 적이 있다면, 그건 내가 그들의 형식화를 아주 많이 훔쳐 왔기 때문이다.
2014년쯤이면 이런 시스템들은 이미 여러 고급 결과를 형식화하는 데 쓰였다. 다소 임의적이지만, 예를 들면 다음과 같다.
이 정리들의 증명은 대체로 길고 정교하게 얽혀 있었다. 그 형식화 역시 대규모 작업이었고, 정리에 남아 있던 마지막 의심까지 줄이는 데 핵심 역할을 했다. 그런데도 수학자들 가운데 큰 인상을 받은 사람은 많지 않았다. 눈에 띄는 예외로는 집합론자인 데이나 스콧(Dana Scott)과 켄 쿠넨(Ken Kunen)이 있었다.
나는 린 자체의 개발사는 잘 모른다. 하지만 그것이 수학 공동체를 어떻게 휩쓸었는지는 조금 안다. 수학자들은 위에서 언급한 증명들 가운데 주류 수학에서 흔히 등장하는 정교한 구성, 이를테면 그로텐디크 스킴(Grothendieck schemes)이나 퍼펙토이드 공간(perfectoid spaces) 같은 것을 다룬 사례가 없다는 점을 미심쩍게 보고 있었다. 톰 헤일스는 이런 정의들의 라이브러리를 구축하자는 생각을 했다. 증명은 제쳐 두고, 일단 정의만 모으자는 것이었다. 그리고 그는 그 목적으로 린을 택했다. 그는 뉴턴 연구소 프로그램 빅 프루프(Big Proof)에서 강연했고, 그 자리에서는 비슷한 생각이 여럿 논의됐다. 케빈 버자드(Kevin Buzzard)는 이 이야기를 듣고 교육에 린을 써 보기로 했다. 나머지는 다들 아는 역사다.
린 공동체의 중요한 행동 하나는 로크가 존재하는 내내 지배해 온 “구성적 증명(constructive proof)” 집착을 버린 것이었다. 내가 앞서 논의했듯 직관주의(intuitionism) 철학은 러셀의 역설(Russell’s paradox) 이후에 등장했다. 그리고 그것은 특히 실수 개념에 특별한 함의를 지녔다. 마르틴뢰프 형 이론(Martin-Löf type theory)은 분명 직관주의적 형식 체계라고 할 수 있다. 그러나 로크에 대해서는 그렇게 말하기가 명확하지 않다. 그런데도 수많은 논문이, 그것이 무관하거나 때로는 말이 되지 않는 경우에도 “구성적 증명”을 언급했다. 이런 집착은 로크의 수학 적용을 가로막았고, 그 분야를 린에게 내주게 했다.
명제는 형식이다(Propositions as types)는 논리 기호 $\forall$, $\exists$, $\to$, $\wedge$, $\vee$와 형 생성자(type constructor) $\Pi$, $\Sigma$, $\to$, $\times$, $+$를 연결하는 이중성이다. 아름답고, 매혹적이며, 이론적으로도 매우 생산적이다. 하지만 이것만이 유일한 길은 아니다. 나는 “증명 보조기(proof assistant)”를 명제는 형식이다 원리에 따라 증명을 검사하는 소프트웨어로 정의하는 경우까지 봤다. 그렇게 정의해 버리면 지난 반세기의 연구 대부분이 단숨에 지워진다. 그러면 로크, 린, 그리고 아그다(Agda)만 남게 된다. 아그다는 마르틴뢰프 형 이론을 구현한다.
오토매스조차 명제는 형식이다의 사례가 아니다. $\Pi$와 $\to$에 해당하는 것이 있기는 하지만, 논리는 일반 논리학 교과서에 나오는 공리와 비슷한 것들로 세운다. 더브라위너르는 이미 50년 전에 여러 이유로 형식(type)과 명제(proposition)의 범주를 구별해 두어야 한다는 점을 이해하고 있었다. 가장 분명한 예로, 나눗셈 연산자는 세 개의 인자를 받아야 하고, $x/y$의 값은 실제로 $y\not=0$이라는 증명에 따라 달라지게 된다. 그는 우리가 증명의 무관성(irrelevance of proofs) 을 가져야 한다고 지적했다.
나는 심지어 “LCF 접근법은 명제는 형식이다와 같은 것”이라고 말하는, 잘 아는 사람들의 말도 들은 적이 있다. 이는 전혀 사실이 아니다. 그리고 이런 헛소리를 바로잡기 위해 블로그 글 하나 전체를 쓴 적도 있다.
로크와 린에는 모두 명제의 정렬(sort)인 Prop이 있다. 이것은 증명 무관성을 제공한다. 특히 어떤 주어진 명제에 대한 모든 증명 객체는 같은 값으로 평가된다. 그렇다면 이런 거대한 항(term)은 필요 없다. 그런데 왜 여전히 유지하는가?
증명 객체가 불필요하다는 사실은 LCF를 위한 로빈 밀너(Robin Milner)의 핵심 발견이었다. 필요한 것은 추상 자료형을 제공하는 프로그래밍 언어, 곧 ML뿐이다. 증명 커널을 추상 자료형 안에 넣고, 추론 규칙을 생성자로 두면 끝이다. 그러면 증명은 동적으로 검사된다. ML의 추상화 장벽 덕분에 속임수는 불가능하다.
한 번은 이 50년 된 아이디어를 명제는 형식이다 세계에서 온 누군가에게 설명하려고 했던 초현실적인 경험이 있다. 학생도 아니었다. 함수형 프로그래밍 분야에서 세계 최고 수준의 전문가 가운데 한 사람이었다. ML 언어의 기원 이야기는 그 사람에게 당연히 핵심 상식이어야 했다. 설명에는 꽤 오랜 시간이 걸렸다. 그리고 결국 그가 납득했는지는 잘 모르겠다. 앞서 내가 말한 폐쇄성의 한 사례다.
램매게던(RAMmageddon)의 시대에, 아무것도 가리키지 않는 거대한 항에 수십 메가바이트를 낭비하는 것은 미친 짓이다. 심지어 이런 쓸모없는 것들을 우아하게 만드는 연구까지 있다.
먼저 뻔한 이야기부터 치우자. 동료들이 린을 쓰고 있고, 그들이 린에 전문성이 있으며, 핵심 전제 지식이 린 라이브러리에 들어 있다면, 당연히 린을 써야 한다.
하지만 자유롭게 선택할 수 있다면, 이 블로그의 중요한 목적 가운데 하나는 이자벨을 고려할 이유를 제시하는 데 있다. 이유는 다음과 같다.
종속형의 핵심 난점은, 제대로 구현하면 형 검사(type checking)가 결정 불가능해야 한다는 데 있다. 이는 동치성(equality)이 결정 불가능하기 때문이다. 초창기에는 이 사실을 당연하게 여겼다. 그러나 1990년 무렵 합의가 바뀌었다. 형 검사를 결정 가능하게 만들기 위해 동치성은 정의적 동치(definitional equality) 또는 내포적 동치(intensional equality) 로 격하됐다. 그래서 $T(N+1)$과 $T(1+N)$이 서로 다른 형이 된다. 이 제약은 증명에 실제 영향을 미친다. 그런데도 정의적 동치를 검사하는 일은 지금도 여전히 계산 부담이 크다.
공정하게 말하자면, 2017년에 누군가 이자벨이 어떤 종류의 수학을 다룰 수 있느냐고 내게 물었다면, 훨씬 조심스럽게 답했을 것이다. 다음과 같은 것을 다루려면 종속형이 필요하다고 쉽게 생각할 수 있기 때문이다.
하지만 우리 몇 사람이 연구를 진행하면서 많은 것을 배웠다. 요령은 모든 것을 억지로 형으로 만들려 하지 않는 데 있다.
린은 많은 것을 올바르게 해낸다. 그리고 린은 충분히 읽기 쉬운 언어가 될 잠재력도 갖고 있다. 심지어 중첩된 증명 블록도 지원한다. 이제 그 사용자 공동체가 이런 기능을 적극 활용해야 한다. 이자벨 사용자들은 대체로 이미 그렇게 하고 있다. 궁극적인 투명성은 컴퓨터가 검사할 수 있는 증명 객체가 아니라, 사람이 실제로 읽을 수 있는 증명 텍스트에 있다.
AI의 등장은 이런 차이를 더욱 또렷하게 만들고 있다. AI가 만든 증명은 대체로 지저분한 편이다. 하지만 슬레지해머를 이용하면 다듬기 쉽다. 내 제한된 경험, 즉 클로드(Claude)를 써 본 경험에 따르면, AI가 내놓는 증명은 구조가 잘 잡혀 있어서 세부가 지나치게 많을 때조차 읽기 쉽다. 무엇이 일어나고 있는지 파악할 수 있고, 어디를 단순화할지도 찾을 수 있다. 최근에는 언어 모델이 직접 슬레지해머를 호출하는 연구도 나왔다. 마지막으로, AI는 읽기 쉬운 구조화된 증명을 한 증명 보조기에서 다른 증명 보조기로 쉽게 번역할 수 있다. 그렇게 되면 무엇을 선택해야 하는지 더는 걱정할 필요가 없어진다.
[웬다 리(Wenda Li)의 의견에 깊이 감사한다!]
[2026년 4월 15일 추가]
어쩌다 보니 또 미자르를 빼먹었다. 미자르(Mizar)와 그 방대한 수학 라이브러리(mathematical library)를 논하지 않고는 수학 형식화의 역사를 온전히 말할 수 없다. 더 안 좋은 점은, 이자벨의 이사르(Isar) 언어가 미자르에서 많은 부분을 빌려왔다는 사실이다. 다음 블로그 글은 미자르에 대해 쓰겠다. 약속한다!