수학 형식화의 역사를 돌아보며 Lean만이 유일한 선택지가 아닌 이유, 그리고 Isabelle을 고려할 만한 이유를 논한다.
23 Apr 2026
[ AUTOMATHLCFHOL systemHOL LightLeanformalised mathematics ]
요즘 수학을 형식화하자고 제안하면 왜 Lean을 사용하지 않는지 설명해야 한다는 말을 들었다. 그리고 그것은 내가 40년 전에 종속 타입 세계를 떠난 이유를 떠올리게 한다. 그 세계의 교조성, 폐쇄성, 그리고 획일성 말이다. Lean은 훌륭한 언어이며 좋은 도구, 큰 라이브러리, 그리고 최근 놀라운 성과를 이룬 거대하고 열정적인 사용자 공동체를 갖추고 있다. 하지만 수학의 형식화 역사는 거의 60년 전으로 거슬러 올라간다는 사실을 잊지 말자. 오늘날의 진보를 둘러싼 과열된 분위기 속에서도, 우리가 어떻게 여기까지 오게 되었는지는 기억해야 한다. 그것은 사람들이 군중을 따라다녀서 이루어진 일이 아니었다.
위에서 언급한 과열 분위기의 일부는 “Lean이 수학의 형식화를 가능하게 만들었다”라는 흔한 주장이다. 미안하지만, 우리는 1968년에 이미 거기에 도달했다. NG de Bruijn의 AUTOMATH에는 이미 필요한 재료의 대부분이 들어 있었다. 1977년에는 Jutting이 이를 사용해 Landau의 _Foundations of Analysis_를 형식화했는데, 이 책은 순수 논리로부터 시작해 복소수의 구성을 다룬다. Jutting은 동치류와 유리수 집합을 사용해 작업했다. 그는 실수 직선의 데데킨트 완비성을 형식적으로 증명했다. 그의 업적은 컴퓨터 성능이 엄청나게 발전했음에도 불구하고 20년 동안 다시 달성되지 못했다. 마침내 1990년대 중반에 John Harrison이 HOL Light를 사용해, Jacques Fleuriot가 Isabelle/HOL을 사용해 다시 실수를 형식화했다.
나는 오늘날 어떤 시스템에서 형식화된 거의 모든 것이 AUTOMATH에서도 형식화될 수 있었으리라고 믿는다. 그것의 주요 단점은 표기법이 정말로 끔찍했다는 점과 자동화가 완전히 없었다는 점이었다. 증명은 길고 읽기 어려웠다.
그럼에도 불구하고, 동치류에 대한 추론에서는 여전히 Rocq보다 더 나았을 가능성이 크다. 후자의 사용자들이 “setoid hell”에 대해 불평하는 동안, Jutting은 자신의 학위논문에서 동치류 형식화를 담담하게 설명한다. 그는 심지어 Landau의 한 장을 두 번째로 형식화하면서, 동치류가 올바른 접근이라고 생각했기 때문에 그것을 채택하기도 했다.
완전히 다른 방향에서는 Robert Boyer, J Moore와 많은 동료들의 작업이 등장했다. 이들은 1973년에 “Proving theorems about LISP functions”라는 제목으로 처음 발표되었고, 목표를 수학이 아니라 코드 검증으로 분명히 제시했다. 그들의 “computational logic”은 일반 수학에 대해서는 분명한 한계를 지니지만, 그렇다고 해서 Gödel의 불완전성 정리에서 quadratic reciprocity, 그리고 Banach–Tarski theorem에 이르기까지 다양한 심오한 결과를 형식화하는 데 사용되는 것을 막지는 못했다. 현재의 구현은 ACL2라고 불리며 주로 하드웨어 검증에 적용된다. 남들과 다르게 하면서도 멀리 갈 수 있다.
획기적인 Edinburgh LCF는 프로그래밍 언어 이론에 좁게 초점을 맞췄지만, 증명 보조기의 _메타언어_로 함수형 프로그래밍 언어를 둔다는 발상은 그래서 ML이라는 이름이 붙었는데, 광범위한 영향을 미쳤다. Cambridge, INRIA, Cornell, 그리고 그 밖의 여러 집단은 ML을 사용해 도구를 만들었고, 그 안에는 HOL, Coq(현재 Rocq), Nuprl의 초기 버전이 포함되었다. HOL 그룹은 하드웨어 검증에 확고하게 집착하고 있었지만, 부동소수점 하드웨어를 검증하려면 실해석이 필요했다. 곧 John Harrison은 코시 적분 공식으로부터 소수정리 같은 제법 본격적인 수학을 증명했다. 그는 가능한 한 많은 유명한 _100 theorems_를 검증하겠다는 과제를 스스로에게 부여했고, HOL Light는 종종 순위표 맨 위에 오른다. Isabelle이 때때로 HOL Light를 앞질렀다면, 그것은 내가 그들의 형식화를 아주 많이 훔쳤기 때문이다.
2014년 무렵에는, 이런 시스템들이 일련의 고급 결과를 형식화하는 데 사용되었다. 다음은 상당히 임의적인 목록이다.
이 정리들은 대부분 길고 복잡한 증명을 가지고 있었다. 이들의 형식화는 대규모 작업이었고, 그 정리들에 대해 남아 있던 의심을 줄이는 데 핵심적이었다. 그럼에도 불구하고, 수학자들 중 인상을 받은 사람은 거의 없었다. 주목할 만한 예외는 둘 다 집합론자인 Dana Scott과 Ken Kunen이었다.
나는 Lean 자체의 발전에 대해서는 아는 바가 거의 없지만, 그것이 어떻게 수학 공동체를 휩쓸었는지에 대해서는 조금 안다. 수학자들은 위에서 언급한 증명들 가운데 주류 수학에서 등장하는 정교한 구성, 예를 들어 Grothendieck schemes나 perfectoid spaces 같은 것을 포함하는 것이 하나도 없다는 점을 미심쩍게 지켜보고 있었다. Tom Hales는 그러한 정의들의 라이브러리를 구축하자는 생각을 했고, 증명은 제쳐두고 정의만이라도 만들자는 것이었으며, 그 목적을 위해 Lean을 선택했다. 그는 Newton Institute 프로그램 Big Proof에서 발표했는데, সেখানে 많은 유사한 아이디어가 논의되었다. Kevin Buzzard는 이 이야기를 듣고 교육에 Lean을 써보기로 결정했다. 나머지는 역사다.
Lean 공동체의 핵심적 행동 가운데 하나는 Rocq를 존재 내내 지배해 온 “구성적 증명”에 대한 기묘한 집착을 버린 것이었다. 내가 이전에 논의했듯이, intuitionism의 철학은 Russell의 역설의 여파 속에서 등장했다. 그것은 특히 실수에 대해 특별한 함의를 가졌다. Martin-Löf type theory는 분명히 직관주의적 형식체계였지만, Rocq에 대해서는 그렇게 분명하지 않다. 그런데도 논문마다 관련이 없거나 때로는 무의미하기까지 한 곳에서 “constructive proof”를 언급했다. 이런 집착은 Rocq의 수학 적용을 방해했고, 그 분야를 Lean에게 내주었다.
Propositions as types는 논리 기호 , , , , 와 타입 생성자 , , , , 를 연결하는 이중성이다. 그것은 아름답고, 매혹적이며, 이론적으로도 생산적이지만, 유일한 게임은 아니다. 나는 “proof assistant”를 propositions as types의 원리에 따라 증명을 검사하는 소프트웨어라고 _정의_하는 것을 본 적이 있다. 그렇게 해버리면 지난 반세기의 연구 대부분이 지워져 버린다. 그러면 Rocq, Lean, 그리고 Agda만 남게 된다. Agda는 Martin-Löf type theory를 구현한다.
AUTOMATH조차 propositions as types의 한 사례가 아니다. 비록 와 의 버전을 갖고 있기는 하지만, 논리는 어떤 논리학 교재에서나 볼 법한 공리들을 사용해 설정한다. De Bruijn은 50년 전에 이미 여러 이유로 타입의 범주와 명제의 범주를 구별해 두어야 한다는 점을 이해하고 있었다. 가장 분명한 예로, 나눗셈 연산자는 세 개의 인수를 받아야 하며, 의 값은 실제로 이라는 증명에 의존하게 될 것이다. 그는 우리에게 _proof irrelevance_가 필요하다고 지적했다.
나는 심지어 “LCF 접근법은 propositions as types와 같은 것이다”라고 말하는, 정보에 밝은 사람들까지 본 적이 있다. 이것은 전혀 사실이 아니며, 이 말도 안 되는 이야기를 바로잡으려는 블로그 글 전체까지 있다.
Rocq와 Lean은 모두 명제의 sort Prop를 포함한다. 이것은 proof irrelevance를 제공하며, 특히 주어진 명제에 대한 모든 proof object는 같은 값으로 평가된다. 그렇다면 이 거대한 항들은 불필요한데도 왜 여전히 유지되는가?
proof object가 불필요하다는 것은 LCF를 위한 Robin Milner의 핵심 발견이었다. 필요한 것은 추상 데이터 타입을 제공하는 프로그래밍 언어, 바로 ML뿐이다. 증명 커널을 추상 데이터 타입 안에 넣고, 추론 규칙을 생성자 자리에 두면, 끝이다! 증명은 동적으로 검사된다. ML의 추상화 장벽 덕분에 속이는 것은 불가능하다.
나는 한때 propositions as types 세계에 있는 누군가에게 이 50년 된 아이디어를 설명하려고 했던 초현실적인 경험을 한 적이 있다. 그는 학생도 아니고 함수형 프로그래밍 분야의 세계적 권위자 중 한 명이었으며, ML 언어의 기원 이야기는 그에게 핵심 상식이어야 할 사람이었다. 꽤 오랜 시간이 걸렸고, 결국 그가 납득했는지는 모르겠다. 이것이 위에서 언급한 폐쇄성의 한 사례다.
RAMmageddon의 시대에, 아무것도 가리키지 않는 거대한 항들에 수십 메가바이트를 낭비하는 것은 터무니없는 일이다. 심지어 이런 쓸모없는 것들을 우아하게 만들려는 연구까지 있다.
먼저 뻔한 이야기부터 치우자. 당신의 동료들이 Lean을 사용하고 있고, 그들이 Lean에 대한 전문성을 가지고 있으며, 핵심적인 선행 결과가 Lean 라이브러리에 있다면, 당연히 Lean을 사용해야 한다.
하지만 자유롭게 선택할 수 있다면, 이 블로그의 핵심 목적 중 하나는 Isabelle을 고려할 이유를 제시하는 것이다. 그 이유는 다음과 같다.
종속 타입의 핵심적 어려움은, 그것을 제대로 하면 타입 검사가 반드시 결정 불가능해져야 한다는 점이다. 그것은 동치성 판단이 결정 불가능하기 때문이며, 초기에는 이 사실이 당연한 것으로 여겨졌다. 그러나 1990년경에 합의가 바뀌었다. 타입 검사를 결정 가능하게 만들기 위해, 동치성은 definitional 또는 intensional equality로 격하되었다. 이것이 바로 과 가 서로 다른 타입인 이유다. 이런 제한은 증명에 실제 영향을 미치지만, definitional equality를 시험하는 일은 지금도 여전히 큰 계산 부담이다.
공정하게 말하자면, 2017년에 Isabelle이 어떤 종류의 수학을 다룰 수 있느냐고 내게 물었다면, 나는 훨씬 더 신중했을 것이다. 다음과 같은 것들을 다루려면 종속 타입이 필요하다고 상상하기 쉽다.
하지만 우리 몇몇은 연구를 좀 해보았고, 많은 것을 배웠다. 요령은 모든 것을 타입으로 억지로 만들지 않는 것이다.
Lean은 많은 것을 올바르게 해냈다. 그리고 Lean은 가독성 있게 될 잠재력을 지니고 있으며, 중첩된 proof block까지 지원한다. 이제 그 사용자 공동체는 Isabelle 사용자들이 대체로 이미 하고 있듯이 이러한 기능을 활용해야 한다. 궁극적인 투명성은 컴퓨터가 검사할 수 있는 proof object가 아니라, 인간이 실제로 읽을 수 있는 proof text다.
AI의 부상은 이런 차이를 더욱 선명하게 만들고 있다. AI가 만든 증명은 대개 지저분한 경향이 있지만, sledgehammer를 사용하면 쉽게 다듬을 수 있다. 내 제한된 경험으로는 Claude를 사용했을 때, 그것들은 구조가 잘 잡혀 있어서 세부가 과도할 때조차 읽기 쉽다. 무슨 일이 벌어지는지 볼 수 있고, 단순화할 방법도 찾을 수 있다. 또한 언어 모델 자체가 sledgehammer를 호출하는 최근 연구도 있다. 마지막으로, AI는 읽기 쉬운 구조화된 증명을 한 proof assistant에서 다른 것으로 손쉽게 번역할 수 있다. 그렇게 되면 어느 것을 선택해야 하는지 더 이상 걱정할 필요가 없어진다.
[Wenda Li의 의견에 깊이 감사드립니다!]
[Added 15 April 2026]
어쩌다 보니, 나는 또다시 Mizar를 빼먹었다. 수학 형식화의 역사는 Mizar와 그것의 방대한 수학 라이브러리에 대한 논의 없이는 완전할 수 없다. 더구나 Isabelle의 Isar 언어는 Mizar에서 많은 것을 빌려 왔다. 다음 블로그 글은 Mizar에 관한 것이 될 것이라고, 이번에는 정말 약속한다!
