9.4 Vibe Proving 實戰#

本節目標#

• 掌握 2024–2026 年一般數學學生/工程師的 AI 輔助 Lean 工作流
• 學會 iterative agent 迴圈：產生 → 編譯 → 修錯
• 親手完成一個實戰範例：用 AI 證明 Cauchy–Schwarz 不等式
• 認識常見失敗模式、prompt 技巧與社群資源

什麼是 vibe proving#

「vibe coding」指靠 AI 生成程式碼、人不逐行理解也能工作的開發方式。vibe proving 是它在數學上的類比：你描述要證什麼，AI 產生 Lean 證明，編譯器保證正確，你可以不逐行理解每個 tactic。

與 vibe coding 的關鍵差異：程式碼錯了會在生產環境爆炸，而證明錯了 Lean 根本不讓它通過。所以 vibe proving 比 vibe coding 更安全——前提是你形式化的「敘述」是對的（這是唯一必須人腦把關的地方，呼應 9.3 節的 AutoFormalization 瓶頸）。

三種使用層次#

flowchart LR
    A[層次一<br/>Copilot 補全] --> B[層次二<br/>直接產 tactic] --> C[層次三<br/>iterative agent]

層次一：Copilot 式補全。 Lean Copilot 或各種 IDE 外掛，在你寫到一半時補下一個 tactic。適合學習期：你能看到補全並決定是否接受。

層次二：直接委託。 把整個定理丟給 Claude/GPT，附上 Lean 版本與錯誤訊息，請它回傳完整證明。適合中短證明。

層次三：iterative agent。 自動化迴圈：agent 產生證明 → 呼叫 Lean 編譯 → 把錯誤訊息餵回 → 修正 → 重試。Hammerspoon 風格的自訂腳本、或現成工具（如 Lean Copilot 的證明搜尋、各家代理）都屬此類。這是 draft–skeleton–prove（9.1 節）的個人版。

實戰：證明 Cauchy–Schwarz#

以下示範層次三的實際操作。你給 AI 的 prompt：

請用 Lean 4 + Mathlib 證明 Cauchy–Schwarz 內積不等式，敘述用 dot_product_le_norm_mul 或自行陳述。若你引入的引理都已在 Mathlib 已有現成敘述，請直接引用。 直接引用。

AI 回傳的骨架與證明（節錄示意）：

import Mathlib

example {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    (u v : V) : |⟨u, v⟩| ≤ ‖u‖ * ‖v‖ := by
  refine le_trans ?_ (norm_inner_le u v)  -- 先用 Mathlib 現成引理試試
  sorry

第一次編譯：sorry 被警告，且這條路線其實方向反了。把錯誤訊息貼回給 AI：

編譯錯誤：norm_inner_le 已經直接給出結論。請直接用它，並刪掉 sorry。

AI 修正：

example {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    (u v : V) : |⟨u, v⟩| ≤ ‖u‖ * ‖v‖ := by
  exact abs_le_abs_of_le (norm_inner_le u v)

第二次編譯：型別不符（abs_le_abs_of_le 參數不對）。繼續回饋錯誤訊息：

example {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    (u v : V) : |⟨u, v⟩| ≤ ‖u‖ * ‖v‖ :=
  le_trans (by simpa using norm_inner_le u v) (by positivity)

第三次編譯通過（或 AI 乾脆找到 Mathlib 已有 abs_inner_le_norm 直接 exact）。整個過程不到五分鐘——而手工在 Mathlib 裡翻找引理，初學者可能要一小時。

注意：這個例子也揭示了 vibe proving 的真相——AI 證明 Cauchy–Schwarz 的主要手段是找到 Mathlib 裡已經有人證好的版本。「證明」的很大一部分是檢索與組裝。

另一個常見練習：組合恆等式，如 ∑ k in range (n+1), k = n * (n+1) / 2，AI 通常會直接用 Finset.sum_range_id 或 Nat.sum_range_id——同樣是檢索而非建構。

常見失敗模式與 prompt 技巧#

prompt 技巧彙整：

1. 給版本資訊：「Lean 4.9.0，Mathlib 2024-XX-XX」
2. 給最小重現：附上完整可編譯的檔案頭（import + 變數聲明）
3. 貼原始錯誤：不要轉述，貼編譯器原文
4. 要求解釋：請 AI 逐行註解證明，強迫它自我檢查
5. 允許多種策略：「先試 aesop，失敗再手工構造」
6. 分而治之：長證明先請 AI 產生 skeleton，逐個 sorry 攻堅

社群資源#

• lean4web：線上 Lean 編輯器，零安裝即可讓 AI 產的程式碼即時驗證
• Lean Zulip（leanprover.zulipchat.com）：new members 頻道對新手極友善，AI 證不通時可以問真人；發問前先貼上完整可重現程式碼是鐵則
• MWE 原則：Minimal Working Example——最小化重現，讓幫你的人（或 AI）不必消化無關 context
• Mathlib 文件站：AI 引用的引理名，去這裡確認真實存在

這算「你證明了它」嗎？#

用 AI 證出的定理，功勞屬於誰？計算機證明四色定理時（1976），數學界爭論了數十年「機器算的算不算證明」；今天的問題更尖銳：連證明本身都是 AI 寫的，你只是形式化了敘述並按下編譯。

保守立場：你證明了「這個敘述在 Lean 的公理系統下成立」，這至少是嚴格的驗證工作。激進立場：不懂證明內容的通過不算理解。這個問題我們留到第 10 章展開——但建議你現在就開始留意：下次 AI 幫你證出什麼，你真的讀懂了嗎？

小結與練習#

小結：vibe proving 有三個層次（補全、委託、agent 迴圈）；核心工作流是「產生→編譯→修錯」迴圈加上人腦審查敘述；失敗模式以幻覺引理與敘述錯誤為主；lean4web 與 Lean Zulip 是必備資源。工具讓形式化平民化，但「證明的所有權」問題才剛開始。

練習：

1. 在 lean4web 上重跑本節的 Cauchy–Schwarz 範例，故意改錯敘述（如把 ≤ 換成 <），觀察 AI 與編譯器各自的反應。
2. 選一個你熟悉的組合恆等式，用 iterative 迴圈讓 AI 證明，記錄你來回的次數與每次失敗原因。
3. 對 AI 產出的每個證明執行 #print axioms，確認無 sorryAx。
4. 寫下你自己的「AI 證明驗收標準」：什麼情況你願意署名？什麼情況不行？帶著這份標準進入第 10 章。