2015 Lean 2 案：第一次正式發布，把白盒自動化變成證明器#

報案人：Leonardo de Moura 與 Soonho Kong。案情：Lean 1 只是 C++ 函式庫，沒人會用。 偵探：de Moura、Kong、Jeremy Avigad、Floris van Doorn。兇器：約束求解的 elaborator ＋ Lua tactic ＋ 可配置核心。

案發現場#

2013 年秋，de Moura 與 Soonho Kong 開始寫碼，目標並不是「再造一個 Coq」：他們想要一個能開發白盒自動化的平台，彌補 Z3 這類黑盒 SMT 求解器「翻來翻去、證明不穩」的毛病（lost-in-translation）。最初的 Lean 只是內嵌在 C++ 裡的函式庫：客戶程式呼叫它來構造可獨立檢查的可信證明，但沒有互動介面、沒有 tactic 前端，連歸納資料型別都缺。

2014 年 6 月 16 日 Lean 0.1 發布，迴響冷淡：HoTT 社群好奇圍觀，但一般數學家覺得「這不是證明器，這是 API」。Kong 2014 年暑假回鍋，Avigad 來微軟訪問一個月，van Doorn 與 von Raumer 開始試用——大家給出同一個診斷：沒有 elaboration（從使用者寫的省略式語法到核心項的精製）、沒有歸納型別與遞迴方程、沒有 tactic 語言，就留不住使用者。

更深的謎題是理論立場：核心要不要支援 HoTT？2014 年的 Lean 選擇把核心做成可配置的，傳統 CIC 與 HoTT 都能跑，想兩邊討好，結果兩邊都不夠順手。

偵查過程#

線索一：Elaboration 即約束求解#

Lean 2 最大的破案手法，是把 elaboration 重新定義為約束求解問題。使用者寫下：

其中 \(? \alpha\) 是待定的元變數（metavariable）。Elaborator 遍歷語法樹，產生一組約束（型別相等、宇宙層級、實例合成），再用統一器＋求解器逐步解出。Kong 的設計讓隱式參數、強制轉換（coercion）、型別類推導全都落在同一個框架裡，而不像 Coq 各自為政。

線索二：Lua tactic 與歸納型別補完#

Lean 2 補上了傳統證明器的標配：歸納資料型別、遞迴定義的方程編譯器、以及用 Lua 寫 tactic 的前端。選 Lua 的理由很務實：輕量、好嵌入 C++。但這也埋下後患——tactic 跑在另一個語言裡，與證明器本體隔著一層翻譯，偵探和警局講不同語言。

一個 Lean 2 風格的證明骨架（概念示意）：

inductive nat : Type
| zero : nat
| succ : nat → nat

definition add : nat → nat → nat
| add zero n := n
| add (succ m) n := succ (add m n)

這在今天看來稀鬆平常，但在 2015 年是 Lean 第一次證明：C++ 核心也能撐起和 Coq 同級的歸納世界。

線索三：CADE 2015 論文與第一批信徒#

2015 年，de Moura、Kong、Avigad、van Doorn、von Raumer 發表《The Lean Theorem Prover (System Description)》（CADE-25）。這篇論文就是 Lean 2 的結案陳詞：小而可獨立實作的可信核心，加上 SMT 式的自動化野心。這篇論文十年後（2025）拿下 CADE Skolem test-of-time 獎，證明當年的立案是對的。

第一批信徒也在这时出现：Avigad 把 Lean 帶進課堂，Ed Clarke（Kong 的博士導師）說「拿 Lean 來開課吧」，van Doorn 用它做 HoTT 形式化。圖書館從零開始累積，emulate 了 Coq 標準函式庫的起步。

結案報告#

Lean 2 破了「能不能用」的案子，卻留下三個新謎團，直接引出 2017-Lean3與mathlib.md：

• tactic 住在外星：Lua 與 Lean 本體脫節，寫自動化的人要同時懂兩套語義，社群擴展不起來。
• elaborator 太聰明反被聰明誤：帶回溯搜尋的 elaborator 效能難測，大檔案一改就全盤重搜。
• HoTT 包袱：可配置核心聽來很美，實作上處處是條件分支，維護成本高昂。Lean 3 最終決定拿掉 HoTT 支援，專心走 CIC 路線。

用探案的話說：Lean 2 證明了警局蓋得起來，也招到了第一批警員，但警員發現對講機（Lua）和辦案系統（C++ 核心）不相通——下一任局長決定換掉整套通訊設備。

證據與工具#

證據一：版本時間軸

證據二：核心公式

Elaboration ＝ 收集約束 \(C_1, \dots, C_n\) ＋ 求解 \(?m\) 。

證據三：偵探工具箱

延伸閱讀：de Moura et al., "The Lean Theorem Prover (System Description)"（CADE 2015）；Leo de Moura《The Making of Lean》投影片（Lean 2 章節）。