10.4 期末專案#

本節目標#

選定一個定理，完成「從定義到完整證明」的形式化專案。
學會選題：依難度分級挑選適合自己的目標。
掌握工作流程：定義 → 敘述 → 骨架 → 填洞 → exact? / AI 輔助。
走完一個完整示範專案： \(\sum_{i=1}^{n} i^2 = \dfrac{n(n+1)(2n+1)}{6}\) 。
認識學習資源，以及 AI 時代的證明學習倫理。

選題指南#

一個好的期末專案：陳述清晰、證明長度適中（30–200 行 Lean）、只用你學過的工具。以下依難度分級：

入門級（一個歸納 + 基本代數）

Pigeonhole 原理的有限版： \(n+1\) 隻鴿子飛進 \(n\) 個洞，必有一洞有兩隻（Mathlib 關鍵字：Finset.exists_lt_card_fiber_of_mul 或 Fintype 相關）。
\(\sum_{i=1}^{n} i = \dfrac{n(n+1)}{2}\) （高斯求和）。
偶數 + 偶數 = 偶數、奇數 × 奇數 = 奇數等奇偶性代數。
\(\binom{n}{k}\) 的對稱性、Pascal 恆等式的直接驗證（10.1 練習）。

中級（需要一點構造或分類）

\(\sqrt{2}\) 是無理數（在有理數/實數上敘述；關鍵字： sqrt、Nat.Prime、奇偶分類）。
質數有無窮多個的完整自證（回顧 05.1，不看解答重寫）。
握手引理（10.2）的完整證明。
演算法正確性：如「集合的插入排序結果有序且為排列」。

進階（結構性證明，需要多次歸納或組合技巧）

AM-GM 不等式：對 \(n = 2\) ， \(\sqrt{ab} \le \dfrac{a+b}{2}\) （實數）；進一步做 \(n = 2^k\) 情形（Mathlib 有 GeomMean 相關內容可對照）。
\(\sum_{i=1}^{n} i^2 = \dfrac{n(n+1)(2n+1)}{6}\) （本節示範）。
二項式定理的組合證明（對 \(n\) 歸納 + Pascal）。
sum of two squares 的第一步：若 \(p \equiv 3 \pmod 4\) 是質數，則 \(p\) 不能寫成兩平方和（關鍵字：Nat.four_dvd_ne、 squares_mod_four；完整兩平方和定理在 Mathlib 為 Nat.sq_add_sq 相關，太難，做第一步即可）。

選題原則：寧可選入門級完整做玩，也不要選進階級做一半。「完整的 60 行」比「sorry 滿天飛的 300 行」更有價值。

工作流程#

步驟 1：定義。 想清楚要用什麼型別表達。求和用 Finset.sum、命題用 Prop、能用 Mathlib 現成定義就不要自造。

步驟 2：敘述。 先把定理寫成 theorem 陳述，證明體先放 sorry。編譯通過（只有 sorry 警告）代表敘述「型別正確」。這一步常暴露敘述本身的錯誤——例如忘了前提 \(n \ge 1\) 。

步驟 3：骨架。 規劃證明結構。歸納題就寫：

theorem demo (n : ℕ) : P n := by
  induction n with
  | zero => -- 基礎
  | succ k ih => -- 歸納步

每個洞先放 sorry，確認結構編譯通過。

步驟 4：填洞。 由內而外，一次填一個洞。基礎情形通常是 simp / decide / ring；歸納步先 rw 掉定義，再 ring_nf 整理，最後用 ih 收尾。

步驟 5：工具輔助。

exact?：把游標放在目標上，讓 Lean 搜尋現成引理。
apply?、rw?：搜尋可套用或可改寫的引理。
#check：確認引理的確切敘述與參數順序。

AI 輔助的使用倫理：用 AI（含 LLM）找引理名稱、解釋錯誤訊息、建議策略，是合理的——就像用 exact? 一樣，是「查資料」。但把 AI 生成的整段證明直接貼上而不理解，就違背了學習目的。本書的規則：每一行你交出去的證明，你都要能逐 token 解釋它在做什麼、為什麼這樣寫能通過。 檢驗法：把 AI 給的證明刪掉，合上視窗，你能重寫出來才算懂。

示範專案：平方和公式#

目標： \(\displaystyle \sum_{i=1}^{n} i^2 = \frac{n(n+1)(2n+1)}{6}\) 。

開發記錄 1：定義與敘述。 求和用 Finset.sum (Finset.range (n+1))。為避免分式，兩邊同乘 \(6\) ：

theorem sum_sq (n : ℕ) :
    6 * ∑ i ∈ Finset.range (n + 1), i ^ 2
      = n * (n + 1) * (2 * n + 1) := by
  sorry

開發記錄 2：骨架。 對 \(n\) 歸納：

theorem sum_sq (n : ℕ) :
    6 * ∑ i ∈ Finset.range (n + 1), i ^ 2
      = n * (n + 1) * (2 * n + 1) := by
  induction n with
  | zero => sorry -- 0 = 0
  | succ k ih =>
    -- 目標：6 * (∑_{i≤k} i² + (k+1)²) = (k+1)(k+2)(2k+3)
    sorry

開發記錄 3：基礎情形。

  | zero => simp

開發記錄 4：歸納步。 先把求和拆開（Finset.sum_range_succ），代入 ih，再交給 ring：

  | succ k ih =>
    rw [Finset.sum_range_succ, ih]
    ring

組合起來：

theorem sum_sq (n : ℕ) :
    6 * ∑ i ∈ Finset.range (n + 1), i ^ 2
      = n * (n + 1) * (2 * n + 1) := by
  induction n with
  | zero => simp
  | succ k ih =>
    rw [Finset.sum_range_succ, ih]
    ring

四個步驟、不到十行——但每一步都踩過「敘述寫錯」「引理名記錯」的坑，這正是專案的價值：除錯的過程就是學習的過程。

延伸：證明原式（帶分式）需要在有理數上敘述；或證明 \(n(n+1)(2n+1)\) 恆被 \(6\) 整除（提示：連續兩整數之一為偶、 \(n \bmod 3\) 分類），這是很好的加分題。

下一步學習資源#

Mathlib 官方文件：https://leanprover-community.github.io/ —— 引理查詢（exact? 的線上版）、命名慣例（Naming Convention 頁面必讀）。
Lean Zulip：https://leanprover.zulipchat.com/ —— 官方論壇， new members 頻道對新手極友善；貼出你的 sorry 與錯誤訊息，通常幾小時內有人回。
Natural Number Game：https://leanprover-community.github.io/nng4/ —— 互動式關卡，把本書 03、04 章的技巧變成遊戲。
Mathlib 100 Theorems：https://leanprover-community.github.io/undergrad.html —— 「100 大學定理」清單中 Mathlib 已形式化的部分，是進階專案的靈感來源。
AI 時代的建議：定理證明是少數「正確性可機器判定」的領域—— AI 可以幫你寫，但 Lean 會誠實地告訴你它對不對。把 Lean 當裁判、 AI 當陪練、你自己當選手；真正長在你腦中的，是你能重寫出來的部分。

全書總結#

我們從「數學證明的兩難」出發：人讀證明會漏看錯誤，人寫證明會跳步。 Lean 給出的答案是把信任外包給一個不知道疲勞、也不接受含糊的裁判。

一路走來：

命題邏輯與集合（02、03 章）：證明即建構，集合即述詞。
自然數與數論（04、05 章）：歸納是萬物之基，質數是主角。
組合、圖、機率（10.1–10.3）：同一個「算兩次」的靈魂，三種不同的舞台。
期末專案（本節）：你已經有資格獨立形式化一個定理了。

形式化數學改變的不是「數學是什麼」，而是「我們如何知道自己對」。願你在未來的某個 sorry 被填上的瞬間，體會到這門手藝的快樂。

小結與練習#

本節重點：

選題分三級，寧小勿大、寧完整勿殘缺。
工作流程：定義 → 敘述（sorry 先行）→ 骨架 → 逐洞填補 → exact? 搜尋。
AI 輔助的界線：查資料可以，代寫不行；檢驗標準是「能否重寫」。
示範專案展示了歸納 + Finset.sum_range_succ + ring 的標準套路。

練習（期末專案）：

完成入門級任選一題（建議：高斯求和），全程遵循五步工作流程，保留每一步的開發記錄。
完成中級任選一題（建議： \(\sqrt{2}\) 無理數），敘述先寫對再證明。
加分題：證明 \(n(n+1)(2n+1)\) 被 \(6\) 整除，並用它把示範專案的分式版敘述補完。
對你在專案中用過的每一條 Mathlib 引理，寫一行註解說明它的敘述（這是練習「逐 token 解釋」的習慣）。
思考題：本書反覆出現「算兩次」與「歸納」兩大母題。請各舉一個書中例子，並說明它們在 Lean 中的實現為何分別對應 Finset 操作與 induction。