跳轉到

2013 Lean 誕生案：de Moura 打造人人可用的證明器#

報案人：SMT 求解器 Z3 之父 Leonardo de Moura。案情：Coq 太難，Isabelle 太老，新人不敢入行。 偵探：de Moura 本人。兇器：C++ 核心 ＋ 依賴型別 ＋ 元程式設計。

案發現場#

2013 年，互動式定理證明界陷入一種尷尬。Coq 與 Isabelle 戰功彪炳，卻各有難解的沉痾：

  • Coq 的 tactic 語言 Ltac 難以擴展，大型函式庫舉步維艱，IDE 體驗停留在上世紀。
  • Isabelle 的 ML 生態封閉，依賴型別支持不足，年輕的程式設計師望而卻步。
  • Z3 等 SMT 求解器在工業界大殺四方，但在數學證明中只能當配角，無法構造可檢查的證明項。

時任微軟研究院研究員的 Leonardo de Moura 剛與 Nikolaj Bjørner 打完 Z3 這場勝仗，心中卻有更大的疑惑：能不能把 SMT 的自動化、程式語言的現代感、依賴型別的表達力，裝進同一個證明器？

2013 年，他在微軟啟動了 Lean 計畫。名字取得謙遜，野心卻極大：Lean，要讓證明變得輕盈。第一版的設計文件開宗明義：效能、可擴展性、美觀的語法，一個都不能少。

同案的背景還有 HoTT 的衝擊：新基礎需要新工具，老證明器對同倫型別論支持有限。Lean 從一開始就把宇宙多態、商型別、擴展性公理納入考量，立意要做「下一個十年的證明器」。

偵查過程#

線索一：C++ 核心與依賴型別的雙刀流#

Lean 的內核是一個用 C++ 撰寫的小型可信核心，負責檢查依賴型別演算（Calculus of Inductive Constructions 的變體）的每一步推理。

其型別系統的核心判斷是：

\[ \Gamma \vdash e : \alpha \]

表示在上下文 \(\Gamma\) 中，項 \(e\) 具有型別 \(\alpha\) 。而依賴函數型別 \(\Pi (x : A), B(x)\) 允許值域 \(B\) 依賴於參數 \(x\) ，從而把命題、謂詞、證明全部統一為項。

Lean 的宇宙階層設計為：

\[ Type_{0} : Type_{1} : Type_{2} : \cdots \]

其中 \(Prop\) 是特殊的不可分宇宙，專門容納命題，以兼顧古典推理與構造性。商型別、選擇公理、函數外延性被作為內建或相容公理引入，務求讓古典數學家也能無痛遷入。

與 Coq 的 OCaml 核心相比，C++ 核心帶來了更快的 elaborator（精製器）與統一器，讓 Lean 在處理大規模代數結構時不再氣喘吁吁。

線索二：元程式設計——偵探可以改造警局#

Lean 最大的破案手法是元程式設計（metaprogramming）。在 Lean 中，tactic 本身就是用 Lean 寫的 Lean 程式，可以直接操作語法樹與證明狀態。

一個最小的 tactic 框架例子如下：

meta def my_intro : tactic unit := do
  t ← target,
  match t with
  | `(%%a → %%b) := intro `h >> skip
  | _ := fail "目標不是蘊含式"
  end

這段程式的意思是：讀取當前目標 \(t\) ，若它形如 \(a → b\) ，則自動引入假設 \(h\) 。其中 \(tactic\) 是一個單子（monad），封裝了證明狀態的讀寫。

更進一步，Lean 允許自訂語法：

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

這種「語言可長大」的特性，讓後來的 mathlib 貢獻者可以發明無數領域專用 tactic，而不必等待核心開發者施恩。這正是 SSReflect 精神在 Lean 世界的轉世。

下表比較了三代證明器的辦案風格：

證明器 核心語言 tactic 擴展 自動化
Coq OCaml Ltac，較難維護 有限
Isabelle Standard ML Eisbach，框架封閉 Sledgehammer 強大
Lean C++，後改 Lean 自舉 Lean 即 tactic，可自訂語法 SMT 風格 ＋simp ＋omega

線索三：從 Lean 3 到 Lean 4 的長征#

Lean 的歷史可分為三個階段：

  • Lean 1 至 Lean 2（2013 至 2016）：驗證概念，吸引 HoTT 社群試用，但函式庫尚小。
  • Lean 3（2017 至 2020）：mathlib 萌芽。Jeremy Avigad、Mario Carneiro 等人發起數學函式庫計畫，採用單一 monorepo、嚴格審查、快速迭代的開源模式。短短數年就累積了數十萬行形式化數學，成為最活躍的證明社群。
  • Lean 4（2021 至今）：de Moura 決定重寫整個系統。新核心不再只是證明器，還是一個通用程式語言與編譯器，支援高效的 C 編譯、FFI、Lake 建構系統。Lean 4 甚至可以自己編譯自己，元程式可以直接編成原生碼執行。關鍵的轉折公式是：證明助理 ＝ 函數式語言 ＋ 驗證核心，Lean 4 把等號右邊的第一項做到了工業級，讓寫 tactic 的體驗與寫 Rust 或 Haskell 一樣愉快。

mathlib 的增長曲線本身就是證據：從 2017 年的數千行，到 2023 年突破百萬行，涵蓋代數、拓樸、分析、數論，成為 AI 訓練的最佳語料，也為 2024 年的 AlphaProof 埋下伏筆。

結案報告#

Lean 並沒有在 2013 年就結案，它真正的結案報告要到 2021 年 Lean 4 發布才算寫完第一章：

  • 降低門檻：VS Code 插件、即時顯示、友善錯誤訊息，讓大學生也能在幾小時內寫出第一個形式化證明。
  • mathlib 生態：證明了「大教堂式」的集中協作可以在形式化數學中成功，改寫了 Coq 與 Isabelle 各自為政的局面。
  • 工業與學術通吃：既有乾淨的依賴型別理論，又有 SMT 式的自動化，成為連接 2008 年 Z3 革命與 2024 年 AI 證明的橋樑。
  • 未竟之業：古典與構造的張力、宇宙管理的複雜性、大規模搜尋的效能，留給了下一代的 AI 偵探去操心。

用探案的話說：de Moura 沒有破完所有案子，但他蓋了一間設備最新、燈光最亮的警局，讓所有後輩都想來辦案。

證據與工具#

證據一：Lean 的經典開場白

theorem and_swap (p q : Prop) : p ∧ q → q ∧ p := by
  intro h
  cases h with
  | intro hp hq => exact ⟨hq, hp⟩

其中 \(p ∧ q\) 是合取引入， \(cases\) 是消去策略， \(⟨hq, hp⟩\) 是匿名構造子。這短短四行展示了 tactic 塊 \(by\) 的工作方式。

證據二：tactic 狀態變遷表

步驟 證明狀態
初始目標 \(⊢ p ∧ q → q ∧ p\)
執行 \(intro\) 後 \(h : p ∧ q ⊢ q ∧ p\)
執行 \(cases\) 後 \(hp : p, hq : q ⊢ q ∧ p\)
執行 \(exact\) 後 無剩餘目標，結案

證據三：偵探工具箱

工具 作用
Lean 核心 C++ 高速檢查器，後改 Lean 自舉
mathlib 最大最活躍的形式化數學函式庫
Lake ＋ VS Code 建構系統與互動式審訊室
Mathport 把 Lean 3 證據自動搬運到 Lean 4 的時光機

延伸閱讀：de Moura et al., "The Lean Theorem Prover (System Description)"（CADE 2015）；《Theorem Proving in Lean》；mathlib 官方文件。