給數學新手的 Lean 導讀：為什麼電腦檢查過的證明比同行審查更可信？

想像一位一絲不苟的數學老師：你交給他一份厚達數百頁的論文，他逐字對照邏輯規則檢查，只要有一步含糊帶過，就絕對不讓你過關。這就是互動式定理證明器（Interactive Theorem Prover）「Lean」的核心角色。

一般電腦負責幫人類「算答案」，Lean 則負責「檢查推理」。你宣稱「因為 A，所以 B」，Lean 會不斷追問依據哪條邏輯規則，並一路追溯至最底層的基本假設（公理）。

Lean 最早由 Leonardo de Moura 於 2013 年在微軟研究院啟動，目前主流版本為 Lean 4，由非營利組織 Lean FRO 負責維護。這套獲得各大研究機構支援的開放原始碼軟體，正逐步成為現代數學界檢驗尖端證明的主流工具。

數學界的信任危機：為什麼頂尖學者開始轉向機器

數百年來，數學界的信任基石建立在「同行審查」之上：作者寫好論文，交由幾位領域專家審讀數月甚至數年。然而現代前瞻證明的篇幅動輒數百頁，牽涉龐雜的跨領域知識，連頂尖專家也難以保證毫無疏漏。

過去三十年間，數起指標性事件暴露出人工審查的極限：

• Wiles 的費馬最後定理漏洞：1993 年 6 月，Andrew Wiles 發表費馬最後定理的證明，震驚全球。但在隨後兩個月的密集審查中，審稿人提出的疑問暴露出關鍵缺口。Wiles 與 Richard Taylor 花費整整一年補救，修正版才於 1995 年 5 月發表。這說明即便頂尖如 Wiles，人類手寫的手稿依然難免存在疏漏，且需耗費龐大人力與時間才能查核補正。
• Voevodsky 發現自身論文錯誤：菲爾茲獎得主 Vladimir Voevodsky 於 1999 年發現自己七年前論文有漏洞。這次經驗促使他投身形式化數學與單值基礎研究，試圖為電腦輔助證明建立更堅固的邏輯底座。他曾在 Quanta 專訪指出：「數學的世界變得非常龐大，複雜度非常高，錯誤有累積的危險。」
• Kepler 猜想與「99% 的確定性」：Thomas Hales 於 1998 年宣稱證明了球體最密堆積猜想，但證明包含 250 頁筆記與 3 GB 程式。12 位審稿人審查四年僅給出「99% 確定正確」的結論。剩餘 1% 疑慮，直到團隊完成 Flyspeck 形式化專案後才徹底消弭。

當證明規模超越人腦負荷，「我看不懂，但我能確定它是對的」這項需求，推動數學家走向形式化驗證。

驗鈔機模型：電腦檢查證明為何值得相信

許多人的第一直覺是：程式難道不會有 Bug 嗎？為什麼電腦說對就是對？Lean 的解答不是要求讀者盲目相信軟體，而是「將必須信任的基礎縮到最小，並公開攤平接受檢驗」。

櫃員與驗鈔機的比喻

想像一家每天經手上萬張現鈔的銀行，主管無法確保每位櫃員都誠實細心，但只要規定所有鈔票進出都必須通過同一台公開透明、規則極簡的驗鈔機，假鈔便無法過關。

在 Lean 的架構中：

• 櫃員：寫證明的數學家、自動化演算法或大型語言模型（AI）。它們可能極度複雜，也可能犯錯。
• 驗鈔機：Lean 的核心（Kernel）。它只依循少數幾條基礎邏輯規則，逐步檢查每個推理步驟。

這項架構遵循荷蘭邏輯學家提出的 de Bruijn criterion：證明的有效性，必須能由一個「小到足以讓人仔細檢查原始程式碼」的獨立核心完成驗證。

 Untrusted layer
 Writers, tactics,
 AI and tools
       |
       | proof terms
       v
 Lean kernel
 (trust root)
       |
       v
 Valid / invalid proof

拒絕「顯然」與跨越信任的合作

人類審稿時最容易忽略的地方，往往是論文中標註「顯然成立」或「同理可證」的跳躍處。Lean 不接受任何模糊空間，每一步都必須給出精確規則。

正因為信任錨定在 kernel 而非人，任何人提交的證明只要通過核心檢查，就是數學上正確的——不必事先認識對方，也不必仰賴聲譽背書。這種嚴格性催生了全新的研究合作模式：

• 液態張量實驗（LTE）：菲爾茲獎得主 Peter Scholze 發起挑戰驗證關鍵定理 9.4，Johan Commelin 團隊歷時一年半完成。Scholze 直言定理 9.4 是他唯一擔心的核心結果，通過形式化驗證後，他對主要證明「已經沒有任何疑慮」，並讚嘆證明助理能在此時程內驗證前瞻研究「簡直瘋狂」。
• 陶哲軒與 PFR 專案：2023 年 11 月，陶哲軒等人證明 PFR 猜想後發起形式化專案，全球社群貢獻者數週內便完成。陶哲軒指出：「它讓大規模的數學合作成為可能，而合作者之間不必事先建立信任。」維護者多次核准素未謀面貢獻者的提交，只因程式碼經機器驗證無誤且確實推進專案。
• 社群數學庫 Mathlib：全球超過 770 位貢獻者已在 Mathlib 中累積逾 13 萬個定義與 28 萬個定理，成為現代形式化數學的共同基石。

程式碼長什麼樣？三個由淺入深的極簡示範

在 Lean 中，寫證明就像寫程式。以下範例均取自官方與社群教材《Mathematics in Lean》：

範例一：證明 $2 + 2 = 4$

theorem easy : 2 + 2 = 4 :=
  rfl

• theorem easy：宣告名為 easy 的定理。
• : 2 + 2 = 4：宣告該定理陳述的命題內容。
• :=：其後為證明主體。
• rfl（reflexivity）：表示「兩邊本質相同」。Lean 將兩端運算式展開至最底層定義，確認一致即通過。若將 4 改為 5，編譯器將立即跳出錯誤。

範例二：陳述費馬最後定理並標註未完成

def FermatLastTheorem :=
  ∀ x y z n : ℕ, n > 2 ∧ x * y * z ≠ 0 → x ^ n + y ^ n ≠ z ^ n

theorem hard : FermatLastTheorem :=
  sorry

這段程式展示了兩項特點：

• ∀ 與 ℕ 精準表達「對所有大於 2 的指數與非零自然數，等式恆不成立」的命題。
• sorry 代表「證明先欠著」。Lean 允許暫時擱置，但會明確標記該定理尚未完工，絕不容許矇混過關。

範例三：證明「偶數的倍數依然是偶數」

例如我們要證明基礎算術命題「對任意自然數 $m$ 與 $n$，若 $n$ 是偶數，則 $m \times n$ 也是偶數」：

example : ∀ m n : Nat, Even n → Even (m * n) := by
  rintro m n ⟨k, hk⟩
  use m * k
  rw [hk]
  ring

• by：宣告進入戰術模式，像在黑板上寫推導步驟一樣引導證明。
• rintro、use、rw：依序引入變數、給出目標結構、代換已知條件。
• ring：呼叫自動化工具處理代數展開與化簡。

關鍵在於：自動化工具（如 ring）只負責「尋找推導路徑」，它給出的每一步細節最終仍必須送回極小的核心逐一檢核，工具本身無法私自放行證明。

機器不是萬能：Lean 絕對不保證的三個盲點

雖然 Lean 提供了極高的邏輯可靠度，但官方手冊明確指出，它絕非萬靈丹，至少存在三個邊界盲點：

盲點一：陳述翻譯錯誤（語意落差）

Lean 只能檢查「證明是否滿足寫下的程式碼陳述」，無法得知「這段程式碼是否符合數學家心中的真實含義」。

在 Google DeepMind 的開放原始碼專案中，Erdős 第 480 題的 Lean 陳述原本應要求變數 $n \ne 0$，卻誤打為 $m \ne 0$。當 $n=0$ 時，公式中的除法觸發了 Lean 的便利規定：系統內「任何數除以 0 一律定義為 0」。結果 AI 迅速找到簡化證明，將不等式化簡為「$0 \le 0$」此等恆真廢話而順利過關。

此外，針對 AI 奧數評測基準題庫 miniF2F 的研究亦發現，超過一半題目的 Lean 陳述與原始題意存在漏掉條件或括號錯誤等落差。

 Intended math idea
         |
         | human translation
         v
 Lean formal statement
         |
         | kernel check
         v
 Proof validates
 the written statement
         |
         v
 Not necessarily
 the intended idea

盲點二：公理依賴性

所有數學皆奠基於基本假設。如果證明暗中引入了互相矛盾的自訂公理，或引用了包含「sorry」的前提定理，核心在局部推導上依然會放行，導致推論建立在不穩定的前提上。Lean 的解方不是消除公理，而是提供透明指令讓使用者一鍵清查定理底層依賴的所有公理與未完前提，確保邊界完全公開。

盲點三：核心自身的潛在 Bug

為防止單一驗證程式出現漏洞，社群發展出多重獨立驗證體系：

• lean4checker：將編譯後的專案重新交由乾淨核心完整過濾。
• nanoda：由獨立社群以 Rust 語言從零實作的第三方檢查器。

不同團隊與不同語言實作的檢查器若均通過驗證，全數踩中相同漏洞的機率便微乎其微。

繁榮背後的代價：反方觀點與形式化的現實瓶頸

隨著 AI 輔助定理證明的爆發（例如 Google DeepMind 的 AlphaProof 與 AlphaGeometry 2 於 2024 年國際數學奧林匹亞（IMO）共同達到銀牌水準；Anthropic 於 2026 年 9 月宣布 Claude 在 11 天內產出逾 1,300 萬行程式碼形式化費馬最後定理），數學界亦浮現深層省思：

1. 驗證不等於新數學發現

主持費馬最後定理形式化專案的 Imperial College London 教授 Kevin Buzzard 在親自編譯驗證 Claude 的證明後直言：「這份形式化只是忠實照著早期文獻走，沒有增加任何東西。」在數學本質上它並未帶來新洞見，它展現的是自動形式化工程的突破。

2. 人類無法閱讀的程式碼巨獸

AI 產出的證明長達 1,340 萬行，在 96 核心（CPU）工作站上的編譯時間將近 Mathlib 的 20 倍。Buzzard 坦言這份程式碼無法實現他原先期望建立的「人類動態探索文件」。機器驗證了「正確」，人類卻未必因此「理解」。

3. 社群審查瓶頸與運算代價

AI 的高產出也對開放原始碼社群造成衝擊。Buzzard 透露，Mathlib 審稿人極不願意審查品質參差不齊的 AI 生成程式碼，社群目前累積超過 3,000 筆待審的程式碼提交（PR），其中逾 600 筆隨時在排隊等待審閱，人類專家的審核時間才是真正瓶頸。

此外，形式化也伴隨著高昂資源消耗。Claude 在 11 天內平行探索完成 FLT 證明，消耗約 60 億個輸出 token（市價估算約 $30 萬美元）；相較之下，Buzzard 主持的五年期人類社群專案則獲得英國研究機構 EPSRC 約 100 萬英鎊資助。形式化工具解決了「可信度」問題，卻尚未解決「理解」與「成本」的挑戰。

4. 數學的終極目的是理解

數學家 Michael Harris 曾撰文提醒形式化熱潮帶來的迷思，強調數學的價值在於人類心智的領會：

「我們玩這個遊戲是為了理解，不是為了贏。」—— Michael Harris

一份無人能讀懂的機器程式碼，即使邏輯無懈可擊，其啟發性依然受限。

 Machine proof
       |
       v
 Correctness
 (high trust)

 Human thought
       |
       v
 Intuition and insight
 (deep understanding)

如何親自體驗：從瀏覽器到解謎遊戲

對於想親身體驗定理證明的讀者，社群提供了非常友善的入門路徑：

• Lean 4 Web Editor：無需安裝任何環境，打開瀏覽器即可直接貼上本文範例執行即時驗證。
• 自然數遊戲（Natural Number Game）：原版由 Kevin Buzzard 與 Mohammad Pedramfar 開發，讀者將從 $0$ 與加法定義出發，像解謎關卡般一步步推導算術性質，是公認最佳的零基礎入門工具。
• 進階學習資源：熟悉基礎後，可進一步閱讀社群教材《Mathematics in Lean》或官方指南《Theorem Proving in Lean 4》。

Lean 終究是一台驗鈔機：它負責確保每張鈔票絕無偽造，但決定這些推理通往何方的，依然是人類數學家的直覺與洞察。當機器替人類扛下繁瑣的查核重擔，數學家或許才能更專注於學問最本質的追求——理解。