跳轉到

2013：Lean 誕生於微軟研究院——Lean 1 的依賴型別理論核心#

事件#

2013 年，Leonardo de Moura（Z3 SMT 解答器的作者）在微軟研究院（Microsoft Research） 啟動 Lean 專案。名稱取自「lean（精簡）」：目標是打造一個核心小而可信的 定理證明器，卻又能作為通用程式語言。第一個公開版本（Lean 1）於 2013 年底問世， 2015 年發表論文〈The Lean Theorem Prover〉（CADE 2015）。

為何重要#

  • 依賴型別理論（dependent type theory）：型別可以依賴值，例如 Vector α n（長度為 n 的 α 陣列）——型別系統直接表達規格。
  • Curry–Howard 對應：命題即型別、證明即程式。定理 P 的證明就是 型別 P 的一個項（term）。
  • universe polymorphism（宇宙多型）：解決 Russell 悖論的 类型宇宙分層（Type 0 : Type 1 : Type 2 ...），讓歸納類型可以跨層複用。
  • unification hints：讓型別類（type class）解析與高階合一更可預測， 補足 Coq type class 推理「有時突然失敗」的缺陷。
  • 小型可信核心（small trustworthy kernel）：核心只負責檢查證明， 前端（elaborator、tactic）再複雜，最終證明都要回放給核心檢查—— 沿襲 LCF 的「trusted kernel」架構。

理論與實用原因#

  • 理論原因：Martin-Löf 類型論（1973–1984）提供了依賴型別的語義； Coq 證明了依賴型別證明器可行，但 Coq 的 Galina（Prop/Set 分離）與 複雜的 elaborator 讓 de Moura 想要更精簡、更統一的基礎。
  • 實用原因：微軟需要驗證大型軟體與數學；de Moura 想把 Z3 的自動化 推理能力帶進互動式證明器——自動化與互動性合一。

程式範例#

依賴型別與 universe polymorphism——Lean 1 的核心語法：

-- 型別可以依賴值：長度 n 是型別的一部分
inductive Vector (α : Type u) : Nat → Type u where
  | nil  : Vector α 0
  | cons : α → {n : Nat} → Vector α n → Vector α (n + 1)

-- 依賴函式：回傳型別依賴輸入值
def head : {α : Type} → {n : Nat} → Vector α (n + 1) → α
  | _, Vector.cons a _ => a

-- universe polymorphism：同一個定義適用所有宇宙層
inductive List' (α : Type u) where
  | nil  : List' α
  | cons : α → List' α → List' α

#check List'            -- List' : Type u → Type u（u 自動多型）
#check List' Nat        -- List' Nat : Type 0
#check List' (Type 0)   -- List' (Type 0) : Type 1——不會產生悖論

命題即型別、證明即程式——定理就是一個函式：

-- 定理 add_zero : n + 0 = n，證明就是建構該等式的一個項
theorem add_zero (n : Nat) : n + 0 = n :=
  Nat.rec (rfl : 0 + 0 = 0) (fun k ih => rfl) n

-- And 的證明就是一對（建構子）——證明與資料共用同一套語法
theorem and_intro_test (p q : Prop) (hp : p) (hq : q) : p ∧ q :=
  ⟨hp, hq⟩   -- 匿名建構子：And.intro hp hq

tactic 模式——證明也可以用腳本寫：

theorem foo (a b : Nat) : a + b = b + a := by
  induction a with
  | zero => simp
  | succ n ih => simp [Nat.succ_add, ih]

對照：Coq 的缺陷——Coq 的 Prop/Set 分離與不可預測的 type class 解析讓使用者常遇到「為什麼這個 instance 找不到」：

(* Coq：universe 衝突與 instance 解析失敗是常見噩夢 *)
Fail Check (fun (A : Type) => A : Type).   (* universe inconsistency *)

彌補了什麼缺陷#

彌補了 Coq「核心與 elaborator 耦合過深、universe 處理不透明、 type class 解析不可預測」的缺陷，也彌補了 Isabelle/HOL「非依賴型別、 無法在型別層面表達規格」的缺陷——Lean 用精簡的依賴型別理論核心 同時兼顧可信度與表達力。

相關條目#