跳轉到

5.1 Mathlib 社群與運作#

本節目標#

  • 認識 Mathlib 的誕生背景：為什麼 2017 年「統一函式庫」的呼聲會出現
  • 理解「單一巨庫（monorepo）」策略的設計動機與代價
  • 了解 Mathlib 的基礎設施：CI、bors、release cadence
  • 掌握貢獻流程：PR、review、deprecate 的完整生命週期
  • 認識社群規模與治理模式，並與 Mizar、Coq 的分散式函式庫對比

一紙呼籲：freek 的 unified library#

2017 年，荷蘭數學家 Freek Wiedijk（形式化數學界人稱「freek」）發表了一篇著名的呼籲文章，主張每個證明助理社群都應該建立一個統一的數學函式庫（unified library），而不是讓各家的數學定理散落在數十個互不相容的專案裡。

他的論點很簡單：形式化數學的價值來自可組合性。若我想引用你證的定理，卻發現你的基礎定義與我的不同，那一切重來。數學本身是層層堆疊的事業，函式庫也必須如此。

Lean 社群是對這個呼籲回應得最徹底的群體之一。

Mathlib 的誕生與單庫策略#

在 Mathlib 出現之前，Lean 3 的數學函式庫分散在多個儲存庫（lean-teaching、各人私有的工具庫等）。2017 年底，社群決定把所有數學相關程式碼合併成一個儲存庫，這就是 mathlib（後來隨 Lean 4 遷移成為 Mathlib）。

單庫策略的核心邏輯：

  • 一組定義，全體共用：所有定理建立在同一套基礎定義上，杜絕「兩個『極限』定義打不通」的災難
  • 重構一次，全體受惠：改一個基礎定義，CI 會強制所有下游使用者也跟著改
  • 審查品質一致：每行程式碼都經過同樣嚴格的數學審查

代價也很明顯：整個函式庫必須一起編譯，任何人的改動都會觸發全庫重建。這逼出了社群一流的 CI 工程。

基礎設施：CI、bors 與 release cadence#

Mathlib 的工程紀律在開源數學界屬於頂級水準：

PR 提出 → CI 檢查（lint、風格、全部編譯）
       → 兩位 reviewer 批准 → bors 合併進入 main
       → nightly release → 數週後 stable release
  • CI：每個 PR 都在雲端完整編譯整個函式庫（快取命中時可大幅加速），並執行風格檢查（lint）：命名、文檔字串、禁用的 API 等都有自動化規則
  • bors：借自 Rust 專案的 merge queue 機制。PR 不是直接合併，而是排隊進入批次（batch），bors 以批次為單位在 main 上重跑測試，避免「單獨通過、合在一起才壞」的組合爆炸問題
  • Release cadence：每隔幾天就有一個 tag 的穩定版本，上游工具（Lean 本體、工具鏈）的升級也以協調好的節奏進行

這套基礎設施是 Mathlib 能長到超過一百萬行還保持一致的關鍵：規模大到人力無法逐一追蹤時，就必須靠機器紀律。

貢獻流程：PR、review、deprecate#

一次典型的貢獻生命週期：

  1. 開 issue 或討論：確認要加入的數學內容的定位與命名
  2. 開 PR：包含新定理、文檔字串（docstring）、必要時附上範例
  3. review：至少需要兩位維護者批准。reviewer 檢查的不只是證明對不對（反正編譯器會檢查），更是定義是否放在正確的抽象層級、命名是否符合慣例、證明是否用了現成引理
  4. bors 合併：進入 merge queue
  5. deprecate：日後若發現更好的定義或命名，不直接刪除舊物，而是標記 deprecated，給下游使用者一個遷移期

Lean 4 內建 deprecation 語法：

@[deprecated "請改用 Nat.pow_le_pow_left（2024-06-12）" (since := "2024-06-12")]
theorem pow_le_pow_left' (h : a ≤ b) (n : ℕ) : a ^ n ≤ b ^ n :=
  Nat.pow_le_pow_left h n

「deprecate 而非刪除」體現了數學函式庫特有的倫理：引用別人的證明鏈時，你不希望鏈條中間的環節某天憑空消失。

社群規模#

到 2020 年代中期，Mathlib 的規模大致是：

  • 數百位貢獻者（以學生與研究者為主力）
  • 超過一百萬行 Lean 程式碼
  • 每年新增數萬條定理與引理
  • 覆蓋範圍從基礎邏輯、分析、代數到表示論、代數幾何的入門地帶

要感受這個規模，最直接的方式是看 Mathlib 目錄結構的一角：

Mathlib/
├── Algebra/          -- 群、環、模、範疇
├── Analysis/         -- 實分析、複分析、泛函分析
├── Combinatorics/    -- 組合數學
├── Geometry/         -- 幾何與流形
├── NumberTheory/     -- 數論
├── Order/            -- 序結構
├── Topology/         -- 拓撲
└── Logic/            -- 邏輯基礎

與 Mizar、Coq 分散式庫的對比#

同時期的其他證明助理走了不同路線：

系統 函式庫模式 特點
Mathlib (Lean) 單一巨庫 一組定義，全庫同編譯，重構徹底
Mizar 集中式文章庫（MML） 歷史最悠久，文章以「文章」為單位發表
Coq 分散式（opam 套件） 各套件（如 math-comp、Coquelicot）各自維護定義

Mizar 的 MML 其實也是集中式，但它缺少 Lean 這種現代 CI 與 PR 審查流程的工程強度；Coq 的分散式模式給予各專案自由，但代價是跨套件的定義相容性要靠人工橋接——想在同一定理裡同時用兩個套件的成果，常會撞上「兩邊的『群』定義不同」。

Lean 社群用單庫策略押注：對數學而言，定義的統一比模組的自由更重要。這個押注在 liquid tensor experiment（見 5.3 節）等專案中獲得了驗證——那樣規模的合作，只有在「所有人共用同一套基礎」的前提下才可能幾個月內完成。

leanprover-community 的治理#

Mathlib 由 leanprover-community 這個 GitHub 組織治理，其運作方式很「開源原教旨」：

  • 維護者群組：約數十位核心維護者擁有合併權，依專長領域分工
  • 沒有 CEO：重大決策（如從 Lean 3 遷移到 Lean 4）透過公開的 Zulip 討論與投票形成共識
  • Zulip 為主要討論場：數學、程式碼、工具各開頻道， newcomer 提問常在數小時內獲得核心開發者親自回覆
  • 歷任 Lean 開發者深度參與：Leonardo de Moura（Lean 原作者）與團隊傾聽數學使用者的需求，語言的演進方向受 Mathlib 實際負載牽引

這形成一個良性循環：語言為數學庫服務，數學庫為語言提供最嚴苛的壓力測試。Mathlib 常被稱為 Lean 生態的「鯨魚」——任何語言或工具的改動，都要先問：Mathlib 還編譯得過嗎？

小結與練習#

本節看到 Mathlib 不只是一個函式庫，而是一套社會契約 + 工程基礎設施的組合：單庫策略保證定義統一，CI 與 bors 保證規模化下的品質，deprecate 機制保證引用鏈的穩定，開放治理保證社群的長期活力。

練習：

  1. 前往 Mathlib GitHub 儲存庫，找一個你熟悉的數學領域目錄，閱讀其中一個檔案的 docstring，觀察命名慣例。
  2. 解釋為什麼 bors 的批次合併機制對「百萬行單庫」特別重要？若沒有它會發生什麼？
  3. 比較單庫與分散式函式庫：如果你要形式化一篇論文，兩種模式下你各會遇到什麼摩擦？
  4. 查看 Mathlib 的 deprecation 檔案 Mathlib/Deprecated/，找一個例子，理解「遷移期」的設計。