4.4 專案：證明 √2 是無理數#

本節目標#

從零設計命題敘述：如何把「 \(\sqrt{2}\) 是無理數」翻譯成自然數層次的 Lean 命題
走一遍完整的開發流程：敘述 → 引理 → 主定理 → 矛盾導出
學習用偶／奇分析與整除（Nat.Prime、dvd）處理分數化簡
拿到一份可編譯的完整程式碼清單，逐行解說
反思：形式化與紙上證明的差異在哪裡

一、命題設計：先決定「說什麼」#

紙上寫法：「假設 \(\sqrt{2} = \frac{p}{q}\) ， \(p, q\) 互質，則 \(p^2 = 2q^2\) ，故 \(2 \mid p\) 、 \(2 \mid q\) ，與互質矛盾。」

直接翻譯需要分數與互質兩個概念。更聰明的設計是把它降級到自然數：

\(\sqrt{2} = \frac{p}{q}\) （ \(q \neq 0\) ）等價於 \(p^2 = 2 q^2\) 。

於是命題可以寫成：

theorem irrational_sqrt_two :
    ¬ ∃ p q : ℕ, q ≠ 0 ∧ p ^ 2 = 2 * q ^ 2 := by

這樣的敘述有三個好處：

完全不需要 ℚ、Irrational、gcd —— 只要 ℕ、乘法、等式
「分數化簡」消失： \(p^2 = 2q^2\) 不可能成立，正是因為左邊的 2 的次方是偶數、右邊是奇數
證明策略單純：反證 + 偶奇分析

（Mathlib 當然已有 Irrational.sqrt two，但本專案的價值在於自己走一遍，只准用初等工具。）

二、開發計畫#

我們把證明切成三個引理，每個都小到一眼能懂：

引理 A：若 \(2 \mid p^2\) ，則 \(2 \mid p\) 。（用 \(2\) 是質數：質數整除乘積必整除某因數）
引理 B：若 \(2 \mid p\) ，則 \(4 \mid p^2\) 。（代數計算，omega / ring 級別）
主定理：反證。 \(p^2 = 2q^2\) 導出 \(2 \mid p\) ；代回得 \(2 \mid q^2\) ，再用引理 A 得 \(2 \mid q\) ；最後 \(2q \neq 0\) 產生矛盾。

第四步「分數化簡」的角色由 引理 A 的反覆使用 扮演：紙上「約去公因數 2」在這裡變成「兩次抽出因數 2」。不需要 Int.gcd，dvd 就夠了。

三、引理 A：質數整除平方必整除底數#

-- 引理 A：2 ∣ p² → 2 ∣ p
lemma two_dvd_of_dvd_sq {p : ℕ} (h : 2 ∣ p ^ 2) : 2 ∣ p := by
  exact Nat.Prime.dvd_of_dvd_pow Nat.prime_two h (by norm_num)

拆解：

Nat.prime_two : Nat.Prime 2： \(2\) 是質數的 Mathlib 事實
Nat.Prime.dvd_of_dvd_pow : p.Prime → p ∣ a^n → n ≠ 0 → p ∣ a：質數的定義性質「整除乘積必整除某因數」推廣到次方
by norm_num：提供 n ≠ 0，這裡是 2 ≠ 0 的平凡計算

這一條正是「 \(p^2\) 是偶數則 \(p\) 是偶數」的嚴格版本。紙上大家覺得顯然，Lean 告訴你：顯然 = 質數定義 + 一點推論。

四、引理 B：整除底數則整除平方的四倍#

主證明裡我們會把 \(p = 2k\) 代入 \(p^2 = 2q^2\) ，得到 \(4k^2 = 2q^2\) ，即 \(q^2 = 2k^2\) 。這步是純代數：

-- 引理 B：(2k)² = 2q² → q² = 2k²
lemma sq_eq_two_sq_of_even {k q : ℕ} (h : (2 * k) ^ 2 = 2 * q ^ 2) :
    q ^ 2 = 2 * k ^ 2 := by
  omega

出乎意料地 omega 就能做： \(p^2\) 與 \(q^2\) 對 omega 而言是原子項（它不理解乘法，但把 q ^ 2 當成一個整體 \(X\) 、k ^ 2 當 \(Y\) ），於是命題 \((2k)^2 = 2X \to X = 2Y\) 中的 \((2k)^2\) 會先被化約 —— 為保險起見，若你的 Mathlib 版本 omega 失敗，改用：

lemma sq_eq_two_sq_of_even' {k q : ℕ} (h : (2 * k) ^ 2 = 2 * q ^ 2) :
    q ^ 2 = 2 * k ^ 2 := by
  simp [sq] at h        -- 展開平方：4 * k² = 2 * q²
  omega                 // 線性了：q² 與 k² 是原子

經驗：遇到「含平方的等式」，先用 simp [sq]（或 ring_nf）降一層，再讓 omega 接手。

五、主定理：矛盾導出#

theorem irrational_sqrt_two :
    ¬ ∃ p q : ℕ, q ≠ 0 ∧ p ^ 2 = 2 * q ^ 2 := by
  intro ⟨p, q, hq0, hp2⟩
  -- 第一步：2 ∣ p
  have h2p : 2 ∣ p := by
    apply two_dvd_of_dvd_sq
    rw [hp2]
    exact Dvd.dvd.mul_right (dvd_refl 2) (q ^ 2)
  -- 第二步：取 p = 2k，代回得 q² = 2k²
  obtain ⟨k, rfl⟩ := h2p
  have hq2 : q ^ 2 = 2 * k ^ 2 := sq_eq_two_sq_of_even hp2
  -- 第三步：2 ∣ q
  have h2q : 2 ∣ q := two_dvd_of_dvd_sq (by rw [hq2]; exact Dvd.dvd.mul_right (dvd_refl 2) (k ^ 2))
  obtain ⟨j, rfl⟩ := h2q
  -- 第四步：q = 2j 與 q ≠ 0 矛盾
  exact hq0 (by omega)

證明骨架解說：

intro ⟨p, q, hq0, hp2⟩：反證的第一半 —— 「不是不存在」就是「存在」，匿名建構子直接解構證據
2 ∣ p^2 的來源：把 hp2 改寫進去後，就是 2 ∣ 2 * q^2，由 Dvd.dvd.mul_right（a ∣ b → a ∣ b * c）與 2 ∣ 2 得到
obtain ⟨k, rfl⟩ := h2p：從 2 ∣ p 取出 \(p = 2k\) ；rfl 讓 Lean 立刻把 p 換成 2 * k
最後 q = 2 * j 與 q ≠ 0：把 hq0 化成 2 * j ≠ 0，omega 收尾

六、完整程式碼清單#

以下清單可直接貼進 Mathlib 專案編譯（不同 Mathlib 版本的引理名可能有微調，編譯錯誤時用錯誤訊息裡的「Did you mean」修正）：

import Mathlib

/-- 引理 A：若 2 整除 p²，則 2 整除 p -/
lemma two_dvd_of_dvd_sq {p : ℕ} (h : 2 ∣ p ^ 2) : 2 ∣ p :=
  Nat.Prime.dvd_of_dvd_pow Nat.prime_two h (by norm_num)

/-- 引理 B：p = 2k 且 p² = 2q²，則 q² = 2k² -/
lemma sq_eq_two_sq_of_even {k q : ℕ} (h : (2 * k) ^ 2 = 2 * q ^ 2) :
    q ^ 2 = 2 * k ^ 2 := by
  simp [sq] at h
  omega

/-- 主定理：不存在自然數 p, q 使 q ≠ 0 且 p² = 2q² -/
theorem irrational_sqrt_two :
    ¬ ∃ p q : ℕ, q ≠ 0 ∧ p ^ 2 = 2 * q ^ 2 := by
  intro ⟨p, q, hq0, hp2⟩
  have h2p : 2 ∣ p := by
    apply two_dvd_of_dvd_sq
    rw [hp2]
    exact Dvd.dvd.mul_right (dvd_refl 2) (q ^ 2)
  obtain ⟨k, rfl⟩ := h2p
  have hq2 : q ^ 2 = 2 * k ^ 2 := sq_eq_two_sq_of_even hp2
  have h2q : 2 ∣ q := by
    apply two_dvd_of_dvd_sq
    rw [hq2]
    exact Dvd.dvd.mul_right (dvd_refl 2) (k ^ 2)
  obtain ⟨j, rfl⟩ := h2q
  exact hq0 (by omega)

#print axioms irrational_sqrt_two
-- 應顯示僅依賴 propext、Classical.choice、Quot.sound

#print axioms 是品質檢查：確認證明沒有偷用 sorryAx。這是紙上證明永遠做不到的自查。

七、與 Mathlib 版本的對照：處理分數化簡的兩條路#

本專案刻意避開了分數。若你堅持用原本的敘述 Irrational (√2 : ℝ)，Mathlib 的路線是：

路線一（gcd）：對 \(p, q\) 取 \(g = \text{gcd}(p, q)\) ，設 \(p = g p'\) 、 \(q = g q'\) 且 \(\gcd(p', q') = 1\) （Nat.gcd_eq_gcd_ab 或 Nat.exists_eq_mul_of_coprime 類工具），代回後 \(2 \mid p'\) 且 \(2 \mid q'\) ，與互質矛盾。這就是紙上「最簡分數」的機械化，成本是搬運 coprime 的 API。
路線二（dvd，本專案）：不做化簡，直接把「可約分」表達成「 \(p^2 = 2q^2\) 有解」，用引理 A 反覆抽出因數 2。因為要處理的質數只有一個，抽出兩次就結束，比一般化的 gcd 便宜得多。

教訓：形式化時，命題敘述的選擇比證明技巧更重要。一個好的敘述能讓「顯然」的部分真的顯然。

八、專案反思#

敘述先行：本專案花最多心思的地方不是證明，而是把 \(\sqrt{2}\) 無理數翻譯成 \(\neg \exists p q, \ldots\) 。敘述設計決定了證明的難度。
引理切塊：把「質數整除平方」抽出來，主定理只剩四步。每個引理都可以單獨測試 —— 這是軟體工程與數學的共通紀律。
自動化的邊界：omega 意外處理了含平方的引理 B（把平方當原子），但引理 A 必須動用質數理論。知道每個工具的能與不能，才能設計出好走的路。
#print axioms：Lean 不只檢查「證完了沒」，還能告訴你「用了哪些公理」。這種等級的自查是形式化的專屬福利。

小結與練習#

本節重點

敘述降級： \(\sqrt{2} = p/q \iff p^2 = 2q^2\) ，讓證明完全停留在 \(\mathbb{N}\)
引理 A（質數整除平方）是核心，來自 Nat.Prime.dvd_of_dvd_pow
「約分」用兩次抽出因數 2 取代，避免 gcd
反證結構：intro ⟨p, q, hq0, hp2⟩ + obtain ⟨k, rfl⟩ + omega 收尾
用 #print axioms 做最終品檢

練習

★☆☆☆☆ 把主定理中的 have h2p ... 改寫成獨立引理 two_dvd_of_sq_eq_two_sq : p ^ 2 = 2 * q ^ 2 → 2 ∣ p，並讓主定理呼叫它。
★★☆☆☆ 用同樣架構證明 \(\sqrt{3}\) 是無理數（把敘述中的 2 * q ^ 2 改成 3 * q ^ 2；引理 A 需要改成「 \(3 \mid p^2 \to 3 \mid p\) 」，用 Nat.prime_three）。
★★★☆☆ 進一步抽象：證明對任意質數 \(r\) ， \(\neg \exists p q : ℕ, q \neq 0 \land p ^ 2 = r * q ^ 2\) （對 \(r\) 使用 Nat.Prime 的假設，引理 A 變成 Nat.Prime.dvd_of_dvd_pow 的一般形式）。
★★★☆☆ 走 gcd 路線：查閱 Mathlib 的 Nat.coprime 與 Nat.Prime.coprime_iff_not_dvd，把「 \(p, q\) 互質且 \(2 \mid p\) 、 \(2 \mid q\) 」寫成矛盾，補完路線一的證明骨架。
★★★★☆ 把主定理與 Real.sqrt_two 連結：查 Real.sq_sqrt，證明 (√2 : ℝ) ^ 2 = 2，然後說明（文字即可）如何由此推出 Irrational (√2 : ℝ)；若有餘力，查 Irrational 的定義把它寫出來。