AI 요약
이 기사는 최근 수학 정형화(Formalisation of mathematics) 분야에서 Lean이 독점적인 지위를 차지하고 있는 현상에 대해 비판적인 시각을 제시합니다. 저자는 현대의 Lean 사용자들이 마치 Lean이 수학 정형화를 처음 가능하게 만든 것처럼 주장하는 '교조주의'와 '순응주의'를 경계해야 한다고 말합니다. 실제로 수학 정형화의 역사는 약 60년 전인 1968년 NG de Bruijn의 AUTOMATH 시스템에서 시작되었으며, 이후 Jutting, John Harrison, Jacques Fleuriot 등 여러 학자가 HOL Light와 Isabelle/HOL 등을 통해 중요한 성과를 거두었습니다. 저자는 과거의 시스템들이 자동화나 표기법에서 한계가 있었음에도 불구하고 이미 깊이 있는 수학적 증명을 수행해냈음을 상기시키며, 현재의 성공이 과거의 다양한 시도들 위에서 가능했음을 잊지 말아야 한다고 조언합니다.
핵심 인사이트
- 역사적 선례: 수학 정형화는 Lean 이전인 1968년 NG de Bruijn이 개발한 AUTOMATH를 통해 이미 시작되었으며, 현대 시스템에 필요한 대부분의 핵심 요소를 갖추고 있었습니다.
- 기념비적 성과: 1977년 Jutting은 AUTOMATH를 사용하여 Landau의 '분석의 기초(Foundations of Analysis)'를 정형화했으며, 이는 복소수 구축과 데데킨트 완비성(Dedekind completeness) 증명을 포함합니다.
- 다양한 접근법의 가치: 1973년 Robert Boyer와 J Moore가 발표한 'LISP 함수에 관한 정리 증명'은 이후 ACL2로 발전하여 괴델의 불완전성 정리부터 바나흐-타르스키 역설까지 폭넓은 수학적 결과를 정형화하는 데 기여했습니다.
- 메타 언어의 탄생: 에든버러 LCF 프로젝트는 정리 증명기의 메타 언어로 함수형 프로그래밍 언어인 ML을 도입하여 HOL, Coq(현재 Rocq), Nuprl 개발의 토대를 마련했습니다.
주요 디테일
- 기술적 한계와 극복: AUTOMATH는 표기법이 난해하고 자동화 기능이 전무하여 증명이 길고 읽기 어려웠으나, 동치류(equivalence classes) 처리에 있어서는 현대의 Rocq(구 Coq) 사용자들이 겪는 '세토이드 지옥(setoid hell)'보다 효율적일 수 있습니다.
- 실수 체계의 재정형화: Jutting의 성취 이후 약 20년이 지난 1990년대 중반에 이르러서야 **John Harrison(HOL Light)**과 **Jacques Fleuriot(Isabelle/HOL)**에 의해 실수 체계가 다시 정형화되었습니다.
- 종속 유형 시스템의 비판: 저자는 Lean이 기반을 둔 종속 유형(Dependent-typed) 세계의 폐쇄성과 군중 심리를 지적하며, 과거에 이 세계를 떠났던 이유가 '교조주의' 때문이었음을 밝힙니다.
- 하드웨어 검증으로의 확장: Boyer-Moore의 접근법은 일반 수학뿐만 아니라 하드웨어 검증 분야에서도 ACL2를 통해 강력한 실용성을 입증하고 있습니다.
향후 전망
- 도구의 다양성 유지: 특정 도구(Lean)에 매몰되지 않고 Isabelle, HOL, ACL2 등 다양한 시스템의 장점을 이해하는 것이 수학 및 소프트웨어 검증 분야의 장기적인 발전에 필수적입니다.
- 학술적 겸손의 필요성: 현대의 기술적 도약이 과거 수십 년간 축적된 연구 성과 위에서 이루어졌음을 인지하고, 새로운 기술이 등장하더라도 과거의 방법론에서 배울 점을 찾는 태도가 요구됩니다.
출처:hackernews