8.2 從 Lean 到 AI 證明#

本章導讀#

本節把視野拉到未來，看 Lean 如何與人工智慧牽手。你會學到錘子 tactic 的概念，AlphaProof 的形式化加搜尋管線，以及規格導向開發與 mathlib 即語料的關鍵洞見。讀完你會明白，為何寫 Lean 也是在為 AI 準備教材。

淺顯說明#

傳統自動化像三個小幫手，錘子則像叫來一整支外援隊。你喊一聲 \(hammer\) ，它就把目標翻譯後丟給外部求解器，找到證明再翻回 Lean 重播，保證每一步都可檢查。

AlphaProof 更進一步，它不只借用現成求解器，還自己學會找證明。流程像打電動：先把自然語言題目翻成 Lean 形式化，再用強化學習瘋狂試探，試出來的正確證明又拿回去訓練，形成越打越強的迴圈。

規格導向開發是另一種思維：先寫規格，再寫程式，最後寫證明。規格就是合約，程式是履約，證明是公證人，AI 負責幫你把三份文件對齊。

最後記住一句話：mathlib 就是 AI 的語料庫。百萬行的人工證明是最高品質的訓練資料，每一行 \(theorem\) 都是給模型的示範題。

正規理論#

錘子 tactic 的架構可用三段式表示：

\[ Goal_{Lean} \xrightarrow{translate} Goal_{ATP} \xrightarrow{search} Proof_{ATP} \xrightarrow{replay} Proof_{Lean} \]

關鍵在最後一步重播，只有能在 Lean 核心中重建的證明才被接受：

\[ ReplayOK \iff KernelCheck(Proof_{Lean}) = true \]

AlphaProof 的管線則多了一個學習迴圈：

\[ Informal \xrightarrow{formalize} Formal \xrightarrow{RL \; search} Candidate \xrightarrow{verify} Theorem \]

其中 \(RL \; search\) 是以 Lean 核心為裁判的強化學習，獎勵函數極其單純：

\[ Reward(p) = 1 \; iff \; KernelAccepts(p) \; else \; 0 \]

規格導向開發的三件套關係如下表：

角色	記號	內容	例子
規格	\(Spec\)	前後條件、不變量	\(Sorted(xs) \land Perm(xs, input)\)
實現	\(Impl\)	符合規格的程式	\(quicksort\)
證明	\(Proof\)	實現滿足規格的證據	\(Correctness(quicksort, Spec)\)

三者的理想關係是：

\[ Impl \models Spec \quad witnessed \; by \quad Proof \]

mathlib 即語料的洞見可用語料規模公式表達：

\[ Corpus = \{(stmt_i, proof_i)\}_{i=1}^{N}, N > 100000 \]

每個二元組都是一次人類專家示範，模型從中學習 \(stmt \to proof\) 的映射。這正是 AlphaProof 能在競賽題上爆發的原因：它站在 mathlib 的肩膀上。

簡易範例#

下面先模擬錘子的精神：把難題外包，再用 Lean 核心驗收。此處用 \(omega\) 與 \(ring\) 扮演迷你錘子，體會分工。

-- 小錘子：先 simp 清理，再用 omega 重播收尾
example (x : Nat) (h : x ≤ 5) : x + 0 ≤ 5 := by
  simp only [Nat.add_zero]
  omega

-- 環等式外包給 ring，核心只檢查正規形一致
example (a b : Int) : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by
  ring

規格導向開發的迷你示範：先寫規格，再寫實現，最後證明相符。

-- 規格：輸出必為偶數
def IsEven (n : Nat) : Prop := ∃ k, n = 2 * k

-- 實現：輸入加倍
def double (n : Nat) : Nat := 2 * n

-- 證明：實現滿足規格
theorem double_is_even (n : Nat) : IsEven (double n) := by
  use n
  rfl

AI 視角的註解：上面的 \(theorem\) 若累積十萬條，就是模型的訓練語料。你每寫一條規格加證明，都在幫未來的 AI 準備考題與答案。

-- 留給 AI 補全的骨架：人類寫規格，AI 填證明
-- spec: reverse (reverse xs) = xs
example (xs : List Nat) : xs.reverse.reverse = xs := by
  simp

歷史典故#

錘子的鼻祖在 Isabelle 世界，Lean 社群亦步亦趨。先看 Z3 與 SMT 革命，沒有 SMT 求解器的成熟，就沒有錘子可搬的救兵。

形式化大工程的信心則來自克卜勒猜想。 Flyspeck 證明機器驗證可以消化人類數百頁的證明，這才讓大家敢把奧賽題也交給機器。

終點就是當代傳奇，見 AlphaProof 與 AI 證明。它把形式化加強化學習搜尋跑成閉環，並直接受惠於 mathlib 這個超大語料庫，正是本節管線圖的現實版。

習題#

畫出錘子 tactic 的三段式流程，並解釋為何最後的重播步驟不可省略， \(KernelCheck\) 在其中扮演什麼角色。
用規格、實現、證明三件套描述一個排序函數的開發流程，並說明 AI 在哪一步最能幫上忙。
解釋為何說 mathlib 即語料，討論語料規模 \(N\) 與證明品質對 AlphaProof 這類模型的影響。