跳轉到

2013：Lean 誕生#

事件#

2013 年，Microsoft Research 的 Leonardo de Moura 發布 Lean 1，目標是打造一個「定理證明器與程式語言合一」的系統：既可形式化數學，也可作為依值型別的通用程式語言執行並驗證程式。2016 年的 Lean 3 幾乎完全重寫（改為 C++、elaborator 重做），成為第一個廣被使用的版本；其數學庫 mathlib 自 2017 年起與語言共同快速成長，如今已涵蓋數萬條形式化定理。

語法/特性加入的理論與實用原因#

1. 依值型別論核心（承襲 CIC 傳統）#

  • 理論原因：Lean 的核心是依值型別演算（Calculus of Inductive Constructions 傳統，承襲 Coq），具備歸納型別、宇宙（universes）、命題即型別，使其同時是邏輯系統與程式語言。
  • 實用原因：一套語言同時服務數學形式化（mathlib）與可驗證程式（編譯為 C 後執行），證明與程式共用同一型別系統。
  • 彌補缺陷：Coq 的核心與 OCaml 底層老舊、編譯速度慢，且難以支援新的型別論變體。

歸納型別與宇宙使 Lean 同時是邏輯系統與程式語言——Type 是資料、Prop 是命題：

-- Lean：歸納型別定義（資料），Prop 中的命題也是歸納型別（證明）
inductive List' (α : Type) where
  | nil : List' α
  | cons : α → List' α → List' α

#check @List'.cons   -- List'.cons : α → List' α → List' α
-- 命題「2 + 2 = 4」本身就是一個型別，其項就是證明
#check (rfl : 2 + 2 = 4)   -- rfl : 2 + 2 = 4，證明即程式

2. 支援 HoTT（同倫型別論）#

  • 理論原因：2013 年 Voevodsky 的 univalent mathematics（Homotopy Type Theory，同倫型別論）需要可支援 univalence axiom 與 higher inductive types 的核心，Lean 2 明確內建 HoTT 模式。
  • 實用原因：univalence 使等價的型別可互相轉換，為結構化數學基礎提供新途徑。
  • 彌補缺陷：Coq/Agda 對 HoTT 的支援是外掛式的，實作不完整或效能不佳。

Lean 2 的 HoTT 模式原生支援 univalence axiom 與 higher inductive types：

-- HoTT 模式：univalence 使等價的型別可互相轉換
-- (ua : A ≃ B → A = B)——型別的等價就是型別的相等
universe u
#check @ua   -- Lean 2 HoTT 模式：ua : A ≃ B → A = B

3. 效能與 elaborator 重做（Lean 3，2016）#

  • 理論原因：依值型別的 elaboration（自型別推導出完整項）需要高效的 unification 與自動化策略。
  • 實用原因：Lean 3 重寫為 C++，elaborator、unifier、tactic 框架全部重做，編譯與互動速度大幅提升，使大型數學庫的開發變得可行。
  • 彌補缺陷：Lean 1/2 的核心效能不足、Coq 編譯大型專案緩慢。

4. 程式語言面向：執行與驗證合一#

  • 理論原因：依值型別語言的程式即證明，Lean 的核心可直接把可執行程式編譯為 C，並以型別系統保證其性質。
  • 實用原因：#eval、#check 提供互動式開發體驗；tactic（如 exact、apply）與證明模式使定理證明如同寫程式。
  • 彌補缺陷：Coq 的程式抽取（extraction）與證明模式分離，開發體驗割裂。
-- Lean 3：定理即型別，證明即項
theorem add_comm : ∀ n m : ℕ, n + m = m + n := by simp [nat.add_comm]

tactic 證明如同寫程式——每一步 apply/exact/induction 都把目標逐步轉化：

-- Lean 3：tactic 模式逐步證明
theorem add_zero (n : ℕ) : n + 0 = n :=
begin
  induction n with n ih,
  { refl },          -- 基底：0 + 0 = 0，由 rfl 證得
  { rw [nat.add_succ, nat.add_zero, ih] }  -- 歸納步：改寫後套用歸納假設
end

程式與證明共用同一型別系統——普通函數與定理可以互相引用、放在同一檔案：

-- Lean：def（程式）與 theorem（證明）同一框架
def square (n : ℕ) : ℕ := n * n

theorem square_nonneg (n : ℕ) : square n ≥ 0 := nat.zero_le _
-- 程式 square 可直接出現在定理敘述中，兩者共用 ℕ 與同一型別論

#eval 提供互動式開發體驗，可驗證程式與證明的行為：

def fact : ℕ → ℕ
  | 0 := 1
  | (n+1) := (n+1) * fact n

#eval fact 10        -- 3628800，直接在編輯器內執行
#check fact          -- fact : ℕ → ℕ

5. mathlib 數學庫與社群#

  • 理論原因：形式化數學需要龐大且互相依賴的定理基礎建設。
  • 實用原因：mathlib（2017 年起整合為單一 monorepo）以一致的風格與審查機制集中維護，成為當代最大的依值型別數學庫之一。
  • 彌補缺陷：Coq 的貢獻分散在多個仓库，缺乏統一標準。

mathlib 提供的基礎使形式化只需站在巨人肩上——引用一條定理即可完成證明：

-- 引用 mathlib 後，複雜定理一兩行證得
-- import Mathlib.Data.Nat.Basic（Lean 4 版 mathlib）
theorem even_plus_odd (n : ℕ) : 2 * n + 1 ≥ n := by
  linarith   -- mathlib/lean 內建的線性算術自動化，一行證得

彌補了什麼缺陷#

Lean 彌補了 Coq 在編譯速度與底層架構上的老舊，並為 HoTT 等新型別論提供了原生支援；「定理證明器 + 程式語言合一」的設計也讓形式化數學與可驗證程式設計首次共享同一套現代化工具鏈。這個路線在 Lean 4（2021）中進一步推向 self-hosting 與 native code，最終成為 AI 時代定理證明（AlphaProof、IMO 驗證）的首選驗證器。

相關條目#