我們是否被 Lean 卡住了？ – 社群對 Lean 證明助理替代方案的觀點
簡短回答：Lean 的主導地位是社會技術鎖定，而非技術必然性
Lean 是現代數學形式化的事實標準，因為它擁有龐大的函式庫（Mathlib）、完善的工具鏈與制度支持。轉向如 Metamath、Isabelle 或 Coq 等替代方案需要相當的函式庫、資金與社群動能，而這些目前皆不足。
1. 為何 Lean 今天感覺「不可避免」
- Mathlib 的規模 – Mathlib 包含約 250 萬行形式化數學，且持續由活躍的社群擴充。僅憑其規模就使 Lean 成為許多研究者最具生產力的環境。
- 全職開發 – Lean Formal Research Organization（FRO）資助開發者，維護線上編輯器，並提供套件管理器、語言伺服器與文件工具。此等專業支援在證明助理中相當罕見。
- 網路效應 – 大多使用證明助理的數學家已在 Lean 上分享其工作，使協作與程式碼重用變得直接。正如一位評論者所說，「the tools we use are a sociological phenomenon。」
- 近期的健全性漏洞 – 雖然 Lean 曾遭遇高調的核心錯誤（嵌套歸納類型），社群迅速修補，顯示即使是大型專案也能從此類挫折中恢復。
“We are ‘stuck with Lean’ as much as we were ‘stuck with Internet Explorer.’” – Jacques Carette (MO answer)
2. 有哪些替代方案以及它們提供什麼
| 系統 | 基礎 | 核心大小 | 顯著優勢 | 目前限制 |
|---|---|---|---|---|
| Metamath / Metamath Zero | 古典 ZFC（或其他公理系統） | ~700 LOC（Python 驗證器） | 核心極小，證明完全透明，具多個獨立驗證器 | 自動化極少，手動證明工作量大，生態系統相較於 Mathlib 極小 |
| Isabelle/HOL | 高階邏輯 | 較大（≈10 k LOC） | 成熟的 IDE（jEdit），強大的自動化，歷史悠久 | 使用者介面感覺過時，對依賴類型關注較少，純數學函式庫較小 |
| Coq | 歸納構造演算（Calculus of Inductive Constructions） | ≈10 k LOC | 強大的 tactics 語言，社群龐大，工業應用 | 純數學函式庫（Coq‑stdlib）遠小於 Mathlib |
| Mizar | 集合論（Tarski‑Grothendieck） | 中等 | 長期的形式化數學歷史 | 現代工具有限，開發節奏較慢 |
| F* | 具副作用程式設計的依賴類型 | 中等 | 設計用於程式驗證，整合 SMT 求解器 | 尚未廣泛應用於純數學 |
社群對替代方案的評論
- Metamath 的吸引力 – 其核心極小且證明完全顯式，提供最高的正確性保證。一位貢獻者指出，驗證 47 000 個定理僅需 6.35 秒，凸顯檢查速度。
- 可用性問題 – 多位回應者強調，證明助理不僅僅是核心；它還包括編輯器、自動補全、套件管理與文件系統。Lean 的生態系在此方面表現卓越，而替代方案往往缺乏可比的前端。
- 基礎偏見 – 有人認為基礎（型別理論 vs. 集合論）的選擇應次於使用者體驗。正如一個回答所說，「foundations are not the operant issue; the majority of usability comes from well‑designed libraries and tooling。」
3. 制度與財務因素
- 金錢重要 – 建置與維護現代證明助理需要全職開發者。Lean FRO 的預算支援持續改進，而大多數替代方案依賴志願者。
- 潛在贊助者 – 如 INRIA 等機構已資助 Coq；類似的支持或能培養有力競爭者。然而，尚無主要機構宣布專門取代 Lean 的計畫。
- 經濟誘因 – 有評論者將此情況比作早期汽車製造商：先行者常被後來更佳設計的產品超越。若大型科技公司將形式驗證視為戰略資產，可能會投資新助理，進而打破 Lean 的壟斷。
4. AI 的角色與未來互操作性
- AI 產生的程式碼 – 最近的 AI 專案已產出超過百萬行 Lean 程式碼，接近 Mathlib 的規模。這暗示 AI 可協助為其他系統啟動函式庫。
- 跨系統翻譯 – 憑藉強大的語言模型，系統間自動翻譯證明（例如 Lean ↔ Metamath）變得可行。lean‑to‑mm0 與 Dedukti 等專案已在探索此方向。
- 驗證管線 – 將相同證明在多個助理中執行可提供額外信心，正如 Hacker News 的評論所示：「What better way to cross‑check a proof than to run it on several different systems simultaneously？」
5. 社會動態與社群鎖定
- 高階數學家的影響 – Kevin Buzzard、Peter Scholze 與 Terry Tao 等人物加速了 Lean 的採用。一則評論警告說：「the adaptation of a particular technology throughout mathematics depends so heavily on whether one particularly famous mathematician uses this technology at a particular point in time。」
- vibe‑coding 的顧慮 – 部分社群成員擔心 Lean 社群文化可能將快速開發置於嚴謹驗證之上，可能導致證明的「vibe‑coding」。
- 可移植性挑戰 – 即使新助理的函式庫規模與 Lean 相當，遷移現有形式化仍非易事；許多需要重新編寫，這是主要障礙。
6. 結論評估
- 技術可行性 – 從技術上建構可行的替代方案是可能的（Metamath 的小型核心、Isabelle 成熟的 IDE、Coq 的 tactics）。主要障礙在於函式庫規模與工具鏈。
- 制度支援 – 若缺乏專門資金與全職開發團隊，替代方案在短期內難以達到 Lean 的成熟度。
- 社群動能 – 目前 Mathlib 的網路效應使 Lean 成為大多數數學家最實用的選擇。
- 未來展望 – AI 驅動的翻譯與潛在企業投資最終可能降低切換成本，但目前數學社群仍實質上「stuck with Lean」。
本綜合僅取自 MathOverflow 的問題、其七個回答以及頂部 Hacker News 評論，並在相關處保留直接引述。