跳轉到

2021：Lean 4 問世#

事件#

2021 年，Leonardo de Moura 與 Sebastian Ullrich 發布 Lean 4，實現「編譯器與語言合一」：Lean 4 的編譯器、巨集系統與 elaborator 全部用 Lean 自己寫（self-hosted）。開發工作逐漸移出 Microsoft，2023 年成立 Lean FRO（Lean Forward Research Organization，由 AWS、 Alonso 等支持）專職維護。同年 mathlib 完成向 Lean 4 的主要遷移；2024 年起，Lean 更成為頂尖數學驗證與 AI 定理證明的事實標準。

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

1. Self-hosted 編譯器#

  • 理論原因：用語言自身實作編譯器是「語言即型別論」的終極展現——編譯器的正確性也處在同一形式化框架內。
  • 實用原因：self-hosting 讓語言功能（如新巨集）可直接用來改進編譯器本身，維護者不需要同時精通 C++ 與依值型別論。
  • 彌補缺陷：Lean 3 的編譯器以 C++ 實作，與語言脫節，難以維護與擴充。
-- Lean 4 的巨集用 Lean 自己寫
syntax "trivial" : tactic
macro_rules
  | `(tactic| trivial) => `(tactic| exact rfl)

self-hosting 的意義：do-notation、pattern matching、甚至編譯器本身都是同一套 Lean 機制。普通 def 程式同樣用 Lean 自己寫：

-- Lean 4：用 Lean 自己寫的程式（編譯器本身也是如此）
def double (n : Nat) : Nat := n + n

#eval double 21   -- 42

Lean 4 的編譯器、巨集系統與 elaborator 全部以 Lean 實作，維護者只需懂一種語言。

2. 巨集與 elaboration 同語言（metaprogramming）#

  • 理論原因：elaboration（項的推導）本身可用一般 Lean 程式定義，語法擴充、tactic、elaborator 統一在一個框架。
  • 實用原因：新增 DSL（如 mathlib 的 ring、simp 等自動化 tactic）門檻大降；do-notation、pattern matching 都是同一機制實作的語法糖。
  • 彌補缺陷：Lean 3 的巨集系統與 elaborator 限制多、文件稀少，擴充核心語法極為困難。

macro_rules 定義語法擴充、#eval 展示元程式設計——都發生在同一個 Lean 程式裡：

-- Lean 4：自訂 DSL 語法與展開
syntax "double" term : term          -- 宣告新語法
macro_rules
  | `(double $n) => `($n + $n)       -- 編譯期把 double 21 展開為 21 + 21

#eval double 21                      -- 42

用 Lean 的 MetaM 在編譯期操作語法樹，門檻大降：

-- Lean 4：元程式設計——在編譯期檢視並操作項
open Lean in
#eval show MetaM _ from do
  let e ← Lean.elabTerm `(1 + 1) none
  pure e   -- elaborateTerm 即 elaborator 本身暴露的 API，普通程式即可呼叫

3. Native code 產生與 C 互操作#

  • 理論原因：編譯到高效原生碼使依值型別程式不再受限於直譯器效能。
  • 實用原因：可與 C 無縫互操作（extern、直接呼叫 C 函式庫），編譯後的 Lean 程式效能接近 C，且 Lean 編譯器本身就以此執行。
  • 彌補缺陷：Lean 3 只能編譯到虛擬機位元碼，效能不足以支撐 self-hosting。

extern 標注讓 Lean 函數直接映射到 C 實作，效能接近 C：

-- Lean 4：extern——同名 C 函式作為原生實作
@[extern "lean_double_impl"]
def double (n : UInt64) : UInt64 := n + n

-- Lean 編譯器本身就是以這種方式 self-hosted 的原生碼

4. AI 時代的定理證明（2024–2025）#

  • 理論原因：Lean 的嚴格核心使 AI 產生的證明可被機器完全驗證——LLM 負責探索，Lean 負責裁決。
  • 實用原因：2024 年 Terence Tao 與 IMO 委員會合作，以 Lean 驗證 IMO 2024 P6 等難題的形式化證明；同年 Google DeepMind 的 AlphaProof 以 Lean 為證明語言達到 IMO 銀牌水準；2025 年的 Gemini Deep Think 等系統更達金獎水準，且都以 Lean（或搭配其形式化格式）為驗證器。Terence Tao 亦發展如 equational（equation prover）等以 Lean 為基礎的證明工具。
  • 彌補缺陷：LLM 幻覺產生「看起來對」的證明；Lean 的形式化驗證使其無所遁形。

mathlib 遷移到 Lean 4 後，依賴基礎建設的證明只需數行：

import Mathlib.Data.Nat.Basic   -- mathlib（Lean 4 版）單行引用

theorem even_sum (n : Nat) : 2 * n = n + n := by
  ring   -- mathlib 提供的 ring tactic，一行證得恆等式

AI 產生的 tactic 證明由 Lean 嚴格裁決——「LLM 起草、Lean 驗證」的雛形：

-- AI 起草 tactic 序列，Lean 核心逐條驗證，錯誤即拒絕
theorem add_assoc' (a b c : Nat) : a + b + c = a + (b + c) := by
  simp [Nat.add_assoc]   -- 由 Lean 核心機器檢查，無法「看起來對」

彌補了什麼缺陷#

Lean 4 彌補了 Lean 3 的巨集系統與 elaborator 限制、以及編譯器不是 self-hosted 的維護困境，同時以 native code 與 C 互操作證明依值型別語言可以兼具極致效能。mathlib 遷移完成後，Lean 成為當代形式化數學的中心，並在 2024–2025 年成為 AI 定理證明（AlphaProof、Gemini Deep Think、Terence Tao 的工具鏈）的標準驗證器——「函數式 + 依值型別 + AI」三線合流。

相關條目#