# 왜 그냥 Lean만 쓰지 않나요?
> Clean Markdown view of GeekNews topic #28989. Use the original source for factual precision when an external source URL is present.
## Metadata
- GeekNews HTML: [https://news.hada.io/topic?id=28989](https://news.hada.io/topic?id=28989)
- GeekNews Markdown: [https://news.hada.io/topic/28989.md](https://news.hada.io/topic/28989.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2026-04-29T07:41:34+09:00
- Updated: 2026-04-29T07:41:34+09:00
- Original source: [lawrencecpaulson.github.io](https://lawrencecpaulson.github.io//2026/04/23/Why_not_Lean.html)
- Points: 1
- Comments: 1
## Topic Body
- **수학 형식화의 역사**는 Lean으로 시작되지 않았고, 거의 60년 전부터 여러 계보의 시스템이 핵심 기법과 성과를 이미 축적해 옴
- 1968년의 **AUTOMATH**, LCF 계열, HOL, Rocq, ACL2, Mizar 같은 도구들은 실해석학부터 소수 정리, 네 가지 색 정리, Kepler 추측까지 폭넓은 형식화를 이뤄 냄
- Lean은 큰 라이브러리와 활발한 공동체를 바탕으로 현대 수학 정의를 빠르게 쌓아 올렸지만, **propositions as types**나 의존 타입이 proof assistant의 유일한 길은 아님
- Isabelle은 **강한 자동화**, 높은 가독성, 의존 타입 회피를 장점으로 내세우며, proof object 없이도 커널의 추상화 장벽으로 증명 검사를 구성하는 LCF 전통을 잇고 있음
- AI가 구조화된 증명을 정리하고 다른 시스템으로 **번역**하는 흐름까지 더해지면서, 한 도구만 절대적 기준으로 보는 부담은 앞으로 더 줄어들 수 있음
---
### 초기 시스템과 다른 계보들
- ## AUTOMATH
- [AUTOMATH](https://lawrencecpaulson.github.io/tag/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](https://doi.org/10.1007/s00165-019-00490-3) 계열의 **computational logic**은 수학이 아니라 코드 검증을 목표로 출발함
- 1973년 논문 [Proving theorems about LISP functions](https://doi.org/10.1145/321864.321875)에서 이 방향이 처음 드러남
- 일반 수학에는 분명한 한계가 있었지만, [Gödel의 불완전성 정리](https://www.cambridge.org/core/books/metamathematics-machines-and-godels-proof/B97649A08193300A18EA41D53FC87214), [quadratic reciprocity](https://doi.org/10.1007/BF00263446), [Banach–Tarski 정리](https://doi.org/10.4230/LIPIcs.ITP.2022.5) 같은 깊은 결과의 형식화에도 쓰였음
- 현재 계보인 ACL2는 주로 **하드웨어 검증**에 적용됨
### LCF 이후의 흐름
- [Edinburgh LCF](https://lawrencecpaulson.github.io/2022/09/28/Cambridge_LCF.html)는 프로그래밍 언어 이론에 집중했지만, 증명 도우미의 **메타언어로 함수형 언어**를 두는 발상은 널리 퍼짐
- Cambridge, INRIA, Cornell 등 여러 그룹이 ML을 사용해 초기 HOL, Coq(현 Rocq), Nuprl 같은 도구를 만듦
- HOL 그룹은 하드웨어 검증에 집중했지만, 부동소수점 하드웨어 검증 때문에 **실해석학**이 필요해졌음
- [John Harrison](https://doi.org/10.1007/978-1-4471-1591-5)은 Cauchy 적분 공식을 통해 **소수 정리** 같은 본격적인 수학 결과를 HOL 계열에서 증명함
- [100 theorems](https://www.cs.ru.nl/~freek/100/)를 가능한 많이 검증하려는 목표 아래 HOL Light는 자주 최상위권에 올랐음
- 2014년까지 이 계열 시스템들은 여러 고급 정리를 형식화했음
- [네 가지 색 정리](https://www.ams.org/notices/200811/tx081101382p.pdf)
- [odd order theorem](https://doi.org/10.1145/2480359.2429071)
- 선택 공리의 [상대적 무모순성](https://doi.org/10.1112/S1461157000000449)
- Gödel의 [두 번째 불완전성 정리](https://rdcu.be/eSZwv)
- Tom Hales의 [Kepler 추측](https://doi.org/10.1017/fmp.2017.1)
- 이 정리들은 대체로 증명이 길고 복잡했고, 형식화 작업도 매우 큰 규모였으며, 정리에 남아 있던 의문을 줄이는 데 핵심 역할을 함
### Lean 공동체의 부상
- 수학자들은 앞선 형식화 성과들이 **Grothendieck schemes**나 **perfectoid spaces** 같은 주류 현대수학의 정교한 구성까지는 다루지 못했다고 봤음
- Tom Hales는 이런 정의들을 라이브러리로 쌓아 올리는 방향을 택했고, 증명보다 **정의의 축적**에 초점을 두며 Lean을 선택함
- 그는 [Big Proof](https://www.newton.ac.uk/event/bpr/) 프로그램에서 이 방향을 발표했고, 비슷한 구상도 함께 논의됨
- Kevin Buzzard가 이를 듣고 교육에 Lean을 써보기로 하면서 이후 확산이 빨라짐
- Lean 공동체의 중요한 전환점으로, Rocq를 오래 지배한 **구성적 증명 집착**에서 벗어난 점이 제시됨
- [직관주의](/2021/11/24/Intuitionism.html)는 Russell의 역설 이후 등장했고, 실수 개념에도 특정한 함의를 가졌음
- [Martin-Löf type theory](https://www.jstor.org/stable/37448)는 분명히 직관주의적 형식주의이지만 Rocq는 그렇게 단순하게 볼 수 없다고 적음
- 그럼에도 Rocq 관련 논문들에서는 구성적 증명이 무관하거나 무의미한 자리에서도 반복적으로 등장했고, 이런 경향이 Rocq의 수학 적용을 가로막으면서 자리를 Lean에 넘겨줬다고 봄
### propositions as types와 LCF의 차이
- [Propositions as types](/2023/08/23/Propositions_as_Types.html)는 논리 기호 **∀, ∃, →, ∧, ∨** 와 타입 생성자 **Π, Σ, →, ×, +** 를 연결하는 이중성임
- 이 틀은 아름답고 이론적으로 생산적이지만 **유일한 길은 아님**
- proof assistant를 propositions as types 원리로 증명을 검사하는 소프트웨어로 한정하면, 지난 반세기 연구의 대부분이 정의 밖으로 밀려남
- 그렇게 되면 Rocq, Lean, [Agda](https://hackage.haskell.org/package/Agda)만 남게 됨
- AUTOMATH조차 propositions as types의 사례는 아니며, Π와 → 비슷한 요소는 있어도 논리는 일반 논리 교재처럼 **공리들로 설정**함
- de Bruijn은 50년 전에 이미 **타입과 명제의 분리**가 필요하다고 봤음
- 대표적으로 나눗셈은 세 인자를 받아야 하고, \(x/y\)의 값은 \(y \ne 0\)의 증명에 의존하게 되므로 **proof irrelevance**가 필요하다고 적음
- **LCF 접근이 propositions as types와 같다는 인식**도 사실과 다르다고 못박음
- [LCF 관련 글](/2022/01/05/LCF.html)
- Rocq와 Lean에는 명제의 sort인 **Prop**가 있으며, 여기서는 같은 명제의 모든 증명 객체가 같은 값으로 평가돼 **proof irrelevance**를 제공함
- 그렇다고 거대한 증명 객체가 사라지는 것은 아니며 실제 시스템에는 여전히 남아 있음
- [Robin Milner의 핵심 발견](https://lawrencecpaulson.github.io/2022/01/05/LCF.html)은 LCF에서 **증명 객체 자체가 필요 없다는 점**이었음
- ML의 **추상 데이터 타입** 안에 증명 커널을 넣고, 추론 규칙을 생성자로 두면 동적으로 증명을 검사할 수 있음
- ML의 **abstraction barrier** 덕분에 부정행위가 불가능하다고 봄
- 거대한 항이 아무것도 지시하지 않는데도 수십 MB를 차지하는 일은 [RAMmageddon](https://www.nature.com/articles/d41586-026-00844-x) 시대에 특히 비합리적으로 다가옴
- 그런 불필요한 항을 더 우아하게 만드는 연구까지 이어지는 점도 비판함
### Isabelle을 고를 이유
- 동료들이 Lean을 쓰고, 팀의 전문성도 Lean에 있고, 필요한 전제 라이브러리도 Lean에 있다면 Lean을 쓰는 편이 자연스러움
- 다만 자유롭게 선택할 수 있다면 Isabelle을 검토할 이유는 분명함
- ## 자동화
- **가장 강력한 자동화**를 장점으로 들며, 일상적인 “hammer”들과 비교해도 **sledgehammer**에 견줄 것은 없다고 평가함
- 컴퓨터 대수 쪽도 별도로 다룰 필요가 있다고 적음
- ## 가독성
- **가독성 면에서 최선의 선택지**로 두며, [Isar 관련 예시들](https://lawrencecpaulson.github.io/tag/Isar)을 근거로 듦
- ## 의존 타입 회피
- **의존 타입이 없기 때문에** universe level과 초보자를 곤란하게 만드는 여러 특이점을 피할 수 있음
- Lean의 mathlib와 Rocq의 SSReflect, Mathematical Components에서도 의존 타입 사용은 권장되지 않는다고 적음
- 의존 타입의 핵심 난점은 제대로 구현하면 **타입 검사 자체가 결정 불가능**해진다는 점임
- 이는 동등성 판정이 결정 불가능하기 때문이며, 초기에는 이 점이 당연하게 받아들여졌다고 적음
- 1990년 무렵부터는 타입 검사를 결정 가능하게 만들기 위해 동등성을 **definitional/intensional equality**로 낮추는 쪽으로 합의가 이동함
- 그 결과 \(T(N+1)\)과 \(T(1+N)\)은 서로 다른 타입이 됨
- 이런 제한은 실제 증명에도 영향을 주며, definitional equality 검사 자체도 여전히 **계산 부담**이 큼
### 의존 타입 없이도 가능한 현대 수학
- 2017년 기준으로는 Isabelle이 어떤 수학까지 감당할 수 있을지 훨씬 더 조심스럽게 봤다고 적음
- 당시에는 다음 같은 주제를 다루려면 의존 타입이 꼭 필요해 보이기 쉬웠음
- [field extensions](https://rdcu.be/cIK3W)
- [p-adic numbers](https://www.isa-afp.org/entries/Padic_Field.html)
- [Grothendieck schemes](https://doi.org/10.1080/10586458.2022.2062073)
- 그러나 [Alexandria 관련 연구](https://www.cl.cam.ac.uk/~lp15/Grants/Alexandria/)를 통해 많은 것을 배웠고, 핵심은 **모든 것을 타입으로 밀어 넣지 않는 것**이라고 정리함
### 앞으로의 방향과 AI
- Lean은 많은 점을 올바르게 잡고 있으며, **중첩된 증명 블록**까지 지원해 잠재적으로 충분히 읽기 좋은 증명 언어가 될 수 있음
- 이제 Lean 공동체가 그런 기능을 실제로 활용해야 하며, Isabelle 사용자들은 이미 대체로 그렇게 하고 있다고 적음
- 컴퓨터가 검사할 수 있는 증명 객체보다 사람이 실제로 읽을 수 있는 **증명 텍스트의 투명성**이 더 중요함
- AI의 부상은 이 차이를 더 선명하게 만듦
- AI가 만든 증명은 지저분한 경우가 많지만 **sledgehammer**로 정리하기 쉽고, 구조가 잘 잡혀 있으면 세부가 과해도 읽을 수 있음
- 그렇게 하면 진행 흐름을 파악하고 더 단순한 형태로 줄이기 쉬워짐
- 최근에는 언어 모델이 직접 sledgehammer를 호출하는 [연구](https://arxiv.org/abs/2604.07455)도 나왔음
- AI는 읽기 쉬운 구조화된 증명을 한 proof assistant에서 다른 proof assistant로 **번역**하는 일도 쉽게 해낼 수 있음
- 그렇게 되면 어떤 시스템을 택할지에 대한 부담 자체가 줄어듦
### Mizar의 누락 보완
- 수학 형식화의 역사는 [Mizar](https://mizar.uwb.edu.pl)와 그 방대한 [수학 라이브러리](https://mizar.uwb.edu.pl/library/) 없이 완전해질 수 없음
- Isabelle의 **Isar 언어**도 Mizar에서 많은 영향을 받았음
- Mizar를 빠뜨린 점을 따로 바로잡으며, 다음 글에서 Mizar를 다룰 예정이라고 적음
## Comments
### Comment 56516
- Author: neo
- Created: 2026-04-29T07:41:35+09:00
- Points: 1
###### [Hacker News 의견들](https://news.ycombinator.com/item?id=47922079)
- HN 독자 대부분은 수학자보다 **프로그래머**에 더 가깝기 때문에, 수학 증명보다 프로그래밍 관점에서 Lean을 보는 편이 더 실용적이라 봄
함수형 프로그래밍 시각으로 Lean을 다루는 책으로 [https://leanprover.github.io/functional_programming_in_lean/]()가 꽤 좋음
나도 Lean을 배우는 중이라 초보자의 **장밋빛 시각**이 좀 있을 수 있지만, 최근 lean-zip 예시처럼 실제 압축/해제 알고리즘 같은 평범한 프로그래머의 코드를 작성하고 증명하는 쪽을 목표로 하고 있음
[https://github.com/kiranandcode/lean-zip/blob/master/Zip/Nat...]()
- 이 책을 읽다가 Lean으로 기본적인 **컴퓨터 대수 단순화기**를 직접 만져봤음
[https://github.com/dharmatech/symbolism.lean]()
C# 코드를 옮긴 포팅이고, Lean의 **표현력**은 놀라울 정도로 큼
- 그런 용도라면 **Dafny**도 비슷한 선택지 아닌가 싶음
예전에 조금 화제가 됐던 걸 봤는데, 이 분야를 최근엔 자세히 따라가진 못했음
- 1990년대에 **소프트웨어 정당성 증명**을 실험했던 사례를 기억하는데, 최종 증명 주석 쪽에서 실제 소프트웨어보다 오류가 더 많이 나왔던 걸로 기억함
그리고 장애물이 두 가지 더 보임. 첫째, 소프트웨어가 **무엇을 해야 하는지** 아는 것 자체가 어렵고, 사용자가 하고 싶은 일과 고객이 돈을 내는 일이 꼭 같지도 않음
둘째, 많은 개발자의 작업 품질이 워낙 낮아서 Java 같은 언어보다 **진리 언어**를 더 잘 다룰 거라고 기대하기 어려움
다만 두 번째는 필요한 주의를 기울이는 AI 시스템으로 대체되면서 사라질 수도 있어서, 그러면 상황이 바뀔 수 있겠음
- **비함수형 프로그래밍**은 어떠냐는 생각이 듦
함수형 프로그래밍도 이미 제쳐둔 수학만큼이나 대부분의 프로그래머에게는 큰 관련이 없다고 봄
- 글쓴이는 **Lean**을 꽤 잘못 이해한 듯하고, 이 분야를 잘 아는 사람처럼 보여서 더 의외였음
Lean이 증명 객체를 그대로 보존하고, 최종적으로는 모든 정의가 펼쳐진 거대한 증명 객체 하나를 검사한다고 보는 듯한데, 실제와는 거리가 멂
Lean은 저자가 LCF의 장점으로 치켜세운 최적화를 사실상 똑같이 구현함. 비유하자면 칠판을 지워가며 증명을 진행하는 방식과 같음
Lean4에서 `def`가 아니라 `theorem`으로 작성하면 그 증명 객체는 더 이상 사용되지 않고, 이건 단순 최적화가 아니라 언어의 핵심 성질임. **theorem은 opaque**함
증명 항이 남아 있다 해도 대화형 모드에서 사용자가 볼 수 있게 하려는 용도일 뿐이고, **커널**은 그 증명 객체가 무엇이었는지 신경 쓰지도 못함
- 이건 구현보다 **개념적 차이**에 더 가까움
LCF에서는 증명과 항이 다른 것이고, 내 생각엔 원래 그래야 함. 이런 **Curry-Howard**식 혼동은 불필요한데, 많은 사람이 그게 컴퓨터로 수학을 하는 유일한 방식인 줄 앎
원하면 LCF에서도 증명을 저장하고 활용할 수 있고, Lean에서도 원하면 최적화로 없앨 수 있을 뿐임
- 종속 타입 이론에서 **증명 객체**는 그냥 어떤 타입을 채우는 항 자체인데, 그렇다면 Lean 구현이 그런 항을 만들지 않고도 증명을 구성할 수 있다는 뜻인지 궁금함
- 맞는 말 같음
**추상 타입** 접근이 메모리를 좀 아끼긴 하겠지만 상수배 차이일 뿐이고 점근적 개선은 아님
Lean이 **수십 MB**를 낭비한다는 식의 불만은 1980~90년대엔 중요했겠지만, 오늘날엔 그만큼 결정적인 장점은 아닐 수도 있어 보임
- Lean이 **함수형 프로그래밍**에 좋다는 말을 많이 듣지만, Agda에서 오면 꽤 투박한 다운그레이드처럼 느껴짐
tactic도 좋다고 하지만 내 경험상 **Coq의 tactic**이 더 강력하고 쓰기 편했음
이게 다 첫인상 편향일 수도 있겠지만, 지금까지는 Lean의 강점이 뭔가 하나를 최고로 잘해서라기보다, 전반적으로 무난하고 **커뮤니티가 크다**는 데 있는 듯함
왜 매력적인지는 알겠지만, 그 대가로 아름다움과 힘이 조금 사라진 느낌이라 아쉽기도 함
- 결국 **네트워크 효과**라는 얘기이기도 함
다만 이런 효과는 그 순간에는 영속적처럼 보여도 실제로는 생각보다 오래가지 않음. 정말 그것만 중요했다면 **Perl**이 지금도 여전히 거물이어야 함
Lean에선 특히 **큰 라이브러리**를 먼저 확보한 점이 큼. Perl에게 CPAN이 그랬던 것과 비슷함
하지만 스케일링 법칙을 보면 대부분의 사용자에게 큰 라이브러리의 가치는 크기의 로그 정도로 늘어날 가능성이 큼
[https://pdodds.w3.uvm.edu/teaching/courses/2009-08UVM-300/do...]()
초반엔 이 격차가 넘을 수 없어 보이지만, 꼭 규모를 따라잡지 않아도 어느 순간부터는 사용성이 더 중요해짐
게다가 **수학 라이브러리 포팅**은 LLM에 잘 맞는 작업이기도 함. 소스는 검증돼 있고, 타깃도 검증 가능하며, 추론 경로도 대체로 옮길 수 있음
반대로 말하면 LLM 덕분에 소수 플랫폼에서 일하는 장벽도 예상보다 낮아짐. 그쪽 라이브러리를 내 플랫폼으로 옮길 수 있다면, 내 증명도 그쪽으로 옮길 수 있을 가능성이 큼
- 오히려 그건 커뮤니티가 마침내 성숙해서 **실제 작업**을 하기 시작했다는 뜻처럼 보임
완벽한 도구가 핵심은 아니고, 충분히 좋은 도구로 일을 해내는 게 더 중요함
- **Agda**는 증명 검사기로는 더 좋지만, 소프트웨어를 만드는 실용적 선택지는 아니라고 봄
Lean은 진짜로 **Haskell의 후계자**가 될 수도 있을 만큼, 소프트웨어 개발용 함수형 언어로 성장할 여지가 있어 보임
- Agda는 조금, Lean은 그보다 더 써봤는데, **수학 증명보다 일반 함수형 프로그램**을 쓰는 건 Lean이 훨씬 쉬웠음
차이는 주로 **도구 지원**에서 났던 것 같음. Agda 문서는 부실하고 시스템에 설치해서 굴리는 것도 번거롭고, 사실상 Emacs를 쓰길 강하게 요구함
반면 Lean은 자체 문서에 `cat` 유틸리티 작성법까지 있고, 전반적으로 훨씬 현대적인 tooling 경험을 줌
- Agda의 함수형 프로그래밍에서 정확히 어떤 점이 좋은지 궁금함
보통 칭찬은 **dependent pattern matching** 쪽에서 많이 듣는데, 그 부분에서는 Lean이 꽤 약하다고 느낌
그래도 일반적인 FP에서도 Agda가 더 친화적이라고 느낀다면, 어떤 점에서 그런지 듣고 싶음
- **Isabelle/HOL**은 언어 자체는 괜찮지만, 툴링에는 데스크톱 중심 접근을 떠나서도 깊은 결함이 있음
언어는 Lean과 다르지 꼭 더 낫다는 건 아니고, 종속 타입에 대한 몇몇 비판에는 동의함
결국 두 언어는 서로 다른 **트레이드오프**를 했고, 그 선택이 각자 영역에서 꽤 효율적인 도구가 되게 만든 듯함. 증명이라는 영역 자체가 넓어서 패러다임마다 강약점이 다르고, Lean은 그중 다른 부분에 특화됐을 뿐임
**Sledgehammer**는 좋지만, Lean에도 비슷한 것이 생기는 건 시간문제 같음
탐색 단계에서는 유용할 수 있어도 리소스를 많이 먹고, 증명을 짧게 만들긴 하지만 공개된 코드에서는 반쯤 마법 같은 `by sledgehammer`보다 **증명의 전체 단계**가 직접 드러나는 편을 더 선호함
반면 Isabelle 자체를 개발하는 일은 Lean보다 훨씬 고통스럽고, 특히 개발자들과 소통하는 과정이 그럼
메일링 리스트에서 **버그는 없고 예상 못 한 동작만 있다**는 식의 태도는 유치하고 비전문적으로 보였음
그리고 Lean과 비슷한 시스템의 RAM 사용량을 비꼬는 것도, Isabelle 쪽의 **메모리 폭식**을 보면 꽤 우스운 얘기임
- 여기서 문제는 **UNSAT 인증서**를 빠르게 검사 가능한 형태로 만드는 일이 전혀 사소하지 않다는 데 있음
사실상 그 자체가 **형식 증명**을 쓰는 것과 비슷한 난이도임
- 마지막으로 확인했을 때 **Isabelle/HOL**은 커스텀 Emacs 모드를 인터페이스로 썼던 걸로 기억함
다른 HOL과 헷갈린 걸 수도 있음
- **Sledgehammer**가 뭔지는 모르지만, 설명만 보면 Mathlib의 `grind`와 거의 같은 도구처럼 들림
[https://leanprover-community.github.io/mathlib4_docs/Init/Gr...]()
- Lean에서 흥미로운 건 **Lean은 언어**인데, 사람들이 주로 이야기하는 건 사실 **Mathlib**이라는 라이브러리라는 점임
Mathlib 제작자들은 꽤 실용주의적으로 보이고, 그래서 Lean 타입 안에 고전 논리를 넣고 직관주의 논리는 일부만 쓰는 듯함
- **배중률**을 설명하면서 든 예시는 틀렸음
"어떤 것이 동시에 참이고 거짓일 수 없다"는 건 배중률이 아니라 **모순율**임
배중률은 `p`가 참이거나 `not p`가 참이라는 뜻임
[https://en.wikipedia.org/wiki/Law_of_noncontradiction]()
- 컴퓨터과학 쪽은 이제 자기들만의 **CSLib**를 만들고 있음
[https://www.cslib.io]() [https://www.github.com/leanprover/cslib]()
직관주의 논리는 본질적으로 **계산 가능한 구성물**로 수학적 논증을 바꾸려는 데 의미가 있으니, 이 문제를 어떻게 다룰지 흥미로움
사실 Lean으로 알고리즘을 쓰는 순간 이미 어떤 형태로든 구성적인 제약 안에 들어가고, 그 목적엔 그 정도 논리만으로 충분할 수도 있음
- **구성주의 수학**을 받아들이는 5단계라는 농담이 떠오름
부정, 분노, 타협, 우울, 수용
Andrej Bauer의 관련 강연과 글도 참고할 만함
[https://www.youtube.com/watch?v=21qPOReu4FI]()
[http://dx.doi.org/10.1090/bull/1556]()
- 여기서 말한 건 **intuitive logic**이 아니라 **intuitionistic logic**이어야 함
- 그런 제약과 막힘이 많은데도, 언제 왜 **직관주의 논리**를 선호하게 되는지 궁금함
- 이런 글은 더 많이 필요하다고 봄
모두가 당연하다는 듯 **그냥 X를 써라**라고 밀어붙이는 집단사고에 대해서도, 적어도 대안을 검토할 만한 설득력 있는 이유는 늘 있음
결국 대안을 버리고 주류를 택하더라도, 지형을 알고 선택하는 편이 더 낫다고 봄
- 완전히 동의하지 않음
지금도 **프레임워크와 대안**을 너무 많이 만들고 있고, 아마 재미있어서 더 그런 듯함
기존 도구를 개선하거나 그냥 실제 일을 진행하는 대신, 언어와 라이브러리와 빌드 도구를 끝없이 늘리는 쪽으로 가는 경우가 많음
언어도 라이브러리도 빌드 툴도 지금의 절반만 있었으면 오히려 더 나았을 거라 봄
- 결국 **상황에 따라 다름**
주류에서 벗어날수록 문서는 줄고, 덜 탐색된 구석 때문에 버그는 늘고, 도움받을 사람도 적어짐
선택지가 스무 개 넘게 쌓이면 평균적으로는 **표준 선택지**를 고르고 넘어가는 게 맞음. 주의력은 유한해서, 의존성마다 조사 보고서를 쓰다 보면 정작 핵심 문제를 못 풂
예외는 두 가지인데, 표준 도구가 내 **사용 사례**에 실제로 맞지 않거나, 표준 도구 자체가 내가 풀려는 핵심 문제와 크게 겹칠 때임
- 이런 논의는 **Python의 과학 컴퓨팅 한계**를 지적하는 글들과 비슷하게 느껴짐
어느 정도 괜찮은 도구 주위에 커뮤니티가 임계질량을 넘겨 모이면, 그게 다른 대부분의 요소를 압도함
모멘텀이 붙고, 튜토리얼과 설명 글과 더 나은 문서가 쌓이면서 사실상 **탈출 속도**에 도달함
Lean은 Terrance Tao 같은 강력한 지지자까지 있어서 지금 딱 그런 위치에 있는 듯함
그래서 "언어 X가 더 낫다"는 말이 완전히 틀린 건 아니어도, 정작 중요한 질문은 놓치기 쉬움
모두가 알고 있고 바로 쓸 수 있고 더 많은 시간이 개선에 투입되는 그 도구보다 **실제로 더 나은가**가 핵심임
결국 **worse is better**, 혹은 좋고 인기 있으면 그 정도로 충분하다는 상황처럼 보임
- LLM이 서로 다른 **형식 체계 번역**을 꽤 효과적으로 가능하게 해줄 거라는 점은 좋은 포인트라고 봄
특히 이 분야는 번역 결과를 상당 부분 **자동 검증**할 수 있어서, 선택 자체가 그리 큰 문제는 아닐 수 있음
- 하지만 **AI 시대**에는 임계질량의 중요성이 훨씬 덜함
AI는 거대한 커뮤니티 라이브러리가 없어도 스스로 코드를 작성할 수 있고, 인터넷에 튜토리얼이 백만 개 떠다니지 않아도 문서와 스펙을 직접 읽음
잡시장이 없는 언어를 피할 필요도 없음. AI는 경력을 쌓는 게 아니라 지금 맡은 일을 하면 되기 때문임
그래서 예전 같으면 기회가 없었을 **소형 언어와 DSL**도 채택될 여지가 커짐
프로그래밍에서 오래 지속된 **언어 단일문화**도 AI가 끝낼 수 있다고 봄
- "오늘날 어떤 시스템으로 형식화된 거의 모든 것은 **AUTOMATH**로도 형식화할 수 있었을 것"이라는 말은, 오늘날 현대 언어로 짜는 건 50년 전 **어셈블리**로도 다 짤 수 있었다고 말하는 것과 비슷함
기술적으로는 맞아도 경제적으로는 전혀 다름
- 어셈블리 언어는 대체로 **튜링 완전**한데, 증명 엔진 쪽에서 그에 대응하는 비교가 정확히 뭔지는 잘 모르겠음
- 15년쯤 전에 **Coq/Rocq**와 몇몇 다른 도구를 만져보려 했는데, 개념보다도 소프트웨어 자체를 도통 이해하기 어려웠음
증명 보조기/대화형 정리증명기에서 이상한 점은, **interactive**라는 성격 때문에 언어와 IDE가 결합된 형태가 되고 실제로도 둘이 강하게 엮인다는 데 있음
그래서 언어만 따로 떼어 말하기가 어렵고, 어떤 환경에서 쓰는지도 같이 봐야 함
나도 VS Code의 열렬한 팬은 아니지만, 수많은 사람이 쓰고 큰돈이 들어가며 다듬어진 **확장 가능한 IDE**가 대안들의 환경보다 훨씬 앞서 있다는 건 분명함
**Natural Numbers Game** 같은 훌륭한 입문 경로도 VS Code의 해킹 가능성과 생태계 덕분에 가능한 것처럼 보임
다만 Lean을 배우며 걱정되는 건 **문법 확장성**이 양날의 검이라는 점임
언어를 익힌 뒤에는 그 언어로 쓴 코드를 읽고 싶어지는데, 프로젝트마다 자기 DSL을 잔뜩 만들기 시작하면 통제가 안 될 수 있음
결국 이건 커뮤니티와 생태계가 얼마나 절제하느냐에 달렸고, 그래서 좀 기대 반 걱정 반으로 보고 있음
- Lean은 수학자들에게 가장 사랑받는 증명 보조기도 아니고, **소프트웨어 형식 검증**에 가장 잘 맞는 도구도 아님
다만 둘 다 그럭저럭 해내고, 대신 가장 얻기 어려운 **모멘텀**을 잡았음
게다가 AI 시대에는 공개된 **인간 작성 코드**의 양이 에이전트가 새 코드를 얼마나 잘 만들어내는지에 직접 영향을 주기 때문에, 그 모멘텀이 더 강해짐