跳轉到

2021 Lean 4 案：用 Lean 重寫 Lean，證明器變成程式語言#

報案人：Lean 3 社群。案情：想改系統就得動 C++，VM 跑不快，擴展撞牆。 偵探：de Moura、Sebastian Ullrich。兇器：自舉編譯器 ＋ 衛生巨集 ＋ 表列型別類求解 ＋ Lake。

案發現場#

2018 年初，mathlib 才約五萬行，de Moura 卻做了最激進的決定：另起私人倉庫，從零重寫 Lean。導火線有三條：第一，Lean 3 的解析器、elaborator、tactic 框架、pretty printer、程式碼產生器大半寫在 C++ 裡，使用者想改就得碰 C++，會兩種語言又懂證明論的人鳳毛麟角。第二，VM 解譯開銷讓高效自動化跑不快， \(ring\) 這類決策程序本該編成原生碼。第三，社群對重寫方向雜音很大，de Moura 索性 stealth mode——關起門來做，Ebner 留守維持 Lean 3，Ullrich 陪他踏上大冒險。

目標寫在白板上：編譯器、elaborator、解析器、tactic 框架、建構系統，全部用 Lean 自己寫；新系統既是可擴展的證明器，也是高效的函數式程式語言。

偵查過程#

線索一：自舉——警局自己蓋自己#

關鍵時間軸本身就是證據：

時間 里程碑
2018-04 Lean 4 開發啟動，首批里程碑：新 runtime、記憶體管理、新 IR 與編譯器、解析器原型
2020-10 Eureka：Lean 4 編譯出 Lean 4（解析器、elaborator、巨集系統、tactic 框架已是 Lean 寫的，僅碼產生器殘留 C／C++）
2021-01 首個 pre-release；CADE 28 論文《The Lean 4 Theorem Prover and Programming Language》；mathlib 約 45 萬行
2023-09-08 Lean 4.0 正式發布；mathlib 移植完成（約 110 萬行，後衝上 150 萬行以上）
2023-07 Lean FRO（Focused Research Organization）成立，非營利、約 20 名工程師，不受單一公司控制

自舉的回報是可擴展性：使用者 \(import\, Lean\) 就能碰到實作系統的內部資料結構，改解析器、改 elaborator、改 pretty printer、改碼產生器，都不必動 C++。

線索二：語言級的三件兇器#

第一件：函數式但原地更新（functional but in-place）＋引用計數 runtime。 Lean 4 程式看來純粹，編譯器在安全時自動複用記憶體，效能逼近 C++，寫自動化不再被 VM 拖累。

第二件：為證明器定製的衛生巨集系統。 \(syntax\) ＋ \(macro\) ＋ \(elab\) 三層：

syntax "my_have " ident " : " term " := " term : tactic

巨集展開保持衛生（不會誤捕綁定變數），領域 DSL 可以長在 Lean 裡。

第三件：表列（tabled）型別類消解。 mathlib 的實例圖又深又大，舊的深度優先搜尋動輒指數爆炸；Lean 4 用表格化消解記住已解子目標，效能起死回生。這是 mathlib 能從 110 萬行衝向 150 萬行還越跑越快的關鍵之一：行數漲五成，檢查反而比 Lean 3 更快。

線索三：生態——Lake、VS Code、FRO#

Lean 4 補上工業級拼圖：Lake 建構系統、FRO 的公開路線圖、上千個 PR 的快節奏開發（2023 年 7 月後主倉庫合併逾 7000 個 PR、25 次以上 release）。mathlib 移植（Mathport＋人力）是社群史詩：2023 年完成，隨即超越 Lean 3 體量。應用也開枝散葉：Reopt 翻譯驗證器、歸納—歸納型別包、車控模型、CSLib、Physlib，乃至軟體驗證成為與數學並列的主戰場。

制度上，FRO 讓 Lean 不再是研究副產品：de Moura 轉任 AWS，Ullrich 共同領導，20 人團隊全職開發，路線圖公開。2025 年，CADE 2015 論文獲 Skolem 獎、Lean 獲 ACM SIGPLAN 程式語言軟體獎——官方蓋章：十年立案，證據確鑿。

結案報告#

Lean 4 的結案不是終點，是轉職：證明器變成通用程式語言，附帶一個驗證核心。

  • 對使用者：寫 tactic 的體驗與寫 Rust／Haskell 一樣愉快，還能編成 C 再編成原生碼載入為外掛。
  • 對數學：mathlib 逾 150 萬行，Schemes、Perfectoid、Liquid Tensor 之後仍在膨脹，成為 AI 證明（見 2024-AlphaProof與AI證明.md）的最佳語料。
  • 對工業：規格導向開發（specification-oriented development）觸手可及，軟體驗證專案大量移入。
  • 未結：官方明言不再重寫，但自動化（2025 年中 v4.22 的類 SMT 白板式 tactic：同餘閉包＋E-matching＋約束傳播＋協作引擎）、效能、AI 整合仍在路線圖上。

探案結語：de Moura 2013 年想蓋一間「輕盈的警局」（見 2013-Lean誕生.md），經過 2015-Lean2正式發布.md 的立案、 2017-Lean3與mathlib.md 的擴編，到 Lean 4 終於讓警局自己會蓋房子——以後要什麼審訊室，警員自己動手。

證據與工具#

證據一：核心判斷（不變的定海神針）

\[ \Gamma \vdash e : \alpha \qquad\text{帥：} Type_{0} : Type_{1} : Type_{2} : \cdots \]

變的是外圍一切皆可擴展：解析器、elaborator、tactic、pretty printer、碼產生器。

證據二：經典開場白（Lean 4 版）

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  cases h with
  | intro hp hq => exact ⟨hq, hp⟩
步驟 證明狀態
初始目標 \(⊢ p ∧ q → q ∧ p\)
\(intro\, h\) 後 \(h : p ∧ q ⊢ q ∧ p\)
\(cases\, h\) 後 \(hp : p,\, hq : q ⊢ q ∧ p\)
\(exact\, ⟨hq,\, hp⟩\) 後 無剩餘目標，結案

證據三：偵探工具箱

工具 作用
自舉編譯器（Lean 寫的 Lean） 高效自動化可編成 C／原生碼
衛生巨集＋ \(elab\) 自訂語法與 DSL
Tabled 型別類求解 mathlib 級實例圖的效能救星
Lake＋VS Code＋FRO 建構、互動審訊室、全職開發團隊

延伸閱讀：de Moura & Ullrich, "The Lean 4 Theorem Prover and Programming Language"（CADE 28, 2021）；Lean FRO 公開路線圖；de Moura《The Making of Lean》Lean 4 章節。