跳轉到

05.1 因數與質數#

本節目標#

  • 理解整除關係 \(a \mid b\) 的形式定義，並熟悉 Nat.dvd 的基本性質。
  • 認識 Lean 4 / Mathlib 中 Nat.Prime 的定義。
  • 用 Lean 證明質數有無窮多個（Euclid 的經典論證）。
  • 寫出一個判斷質數的小工具，並與 Nat.Prime 掛勾。

整除的定義#

在數論中，我們說 \(a\) 整除 \(b\) （記作 \(a \mid b\) ），是指存在整數 \(k\) 使得 \(b = a \cdot k\) 。例如 \(3 \mid 12\) ，因為 \(12 = 3 \times 4\) ；但 \(5 \nmid 12\) 。

在 Mathlib 中，這個關係是廣義的 Dvd 類別，自然數上的版本就是 Nat.dvd：

-- Mathlib 中的定義（概念示意）
-- a ∣ b ↔ ∃ k, b = a * k
example (a b : ℕ) : a ∣ b ↔ ∃ k, b = a * k := dvd_iff_exists_eq_mul_left

注意 Lean 中 ∣ 是一個符號記號（輸入方式：\mid），3 ∣ 12 讀作「3 整除 12」。

整除的基本性質#

整除最重要的兩條性質是反身性與傳遞性：

  • 反身性： \(a \mid a\) ，因為 \(a = a \cdot 1\) 。
  • 傳遞性：若 \(a \mid b\) 且 \(b \mid c\) ，則 \(a \mid c\) 。
example (a : ℕ) : a ∣ a := Nat.dvd_refl a

example (a b c : ℕ) (hab : a ∣ b) (hbc : b ∣ c) : a ∣ c :=
  Nat.dvd_trans hab hbc

其他常用的性質：

example (a : ℕ) : 1 ∣ a := Nat.one_dvd a

example (a : ℕ) : a ∣ 0 := dvd_zero a

-- 若 a ∣ b 且 a ∣ c，則 a ∣ b + c
example (a b c : ℕ) (hab : a ∣ b) (hac : a ∣ c) : a ∣ b + c :=
  Nat.dvd_add hab hac

-- 若 a ∣ b，則對任意 k，a ∣ k * b
example (a b k : ℕ) (hab : a ∣ b) : a ∣ k * b :=
  Nat.dvd_mul_of_dvd_right hab k

這些引理的命名都有規律：dvd_refl、dvd_trans、dvd_add、dvd_mul_of_dvd_right， 讀者可以從名稱猜出內容，這正是 Mathlib 命名規範的威力。

質數的定義#

定義：自然數 \(p > 1\) 稱為質數（prime），若 \(p\) 的正因數只有 \(1\) 和 \(p\) 本身。

等價的說法：若 \(p = a \cdot b\) ，則 \(a = 1\) 或 \(b = 1\) 。

Mathlib 中 Nat.Prime p 的定義正是後者：

-- Mathlib 定義（示意）
-- def Nat.Prime (p : ℕ) : Prop :=
--   2 ≤ p ∧ ∀ a b : ℕ, p = a * b → a = 1 ∨ b = 1

example : Nat.Prime 2 := by decide
example : Nat.Prime 3 := by decide
example : ¬ Nat.Prime 4 := by decide
example : ¬ Nat.Prime 1 := by simp [Nat.Prime]

decide 能處理這些具體數字，是因為 Nat.Prime 是可判定的命題（對小數字而言）。

篩法的直覺#

要找出不超過 \(n\) 的所有質數，Eratosthenes 篩法（sieve）的想法是：

  1. 列出 \(2, 3, 4, \dots, n\) 。
  2. 取最小的未刪數 \(2\) ，它是質數；刪掉所有 \(2\) 的倍數。
  3. 取下一個未刪數 \(3\) ，它是質數；刪掉所有 \(3\) 的倍數。
  4. 重複，直到剩下的最小未刪數超過 \(\sqrt{n}\) 。

正確性的關鍵觀察：若 \(n\) 是合數，則 \(n = a \cdot b\) 且 \(1 < a \le b\) ， 於是 \(a \le \sqrt{n}\) ，即 \(n\) 必有一個不超過 \(\sqrt{n}\) 的質因數。

-- 合數必有大於 1 且小於自身的因數
example (n : ℕ) (hn : ¬ Nat.Prime n) (hn1 : 1 < n) :
    ∃ m, m ∣ n ∧ 1 < m ∧ m < n := by
  rcases Nat.exists_eq_mul_of_not_prime hn hn1 with ⟨a, b, heq, ha, hb⟩
  exact ⟨a, ⟨a, by rw [heq]⟩, ha, by have := Nat.lt_of_mul_lt_mul_left hb; omega⟩

用 Lean 形式化完整的篩法需要陣列操作，超出本節範圍，但上面這個「合數有真因數」 的引理正是篩法與下一節唯一分解定理的基石。

質數無窮多：Euclid 的論證#

定理（Euclid）：質數有無窮多個。

Euclid 的證明思路：假設質數只有有限個 \(p_1, \dots, p_k\) ，考慮 \(N = p_1 \cdot p_2 \cdots p_k + 1\) 。任何 \(p_i\) 都不整除 \(N\) （因為 \(N \div p_i\) 餘 1）， 所以 \(N\) 的質因數不在名單中，矛盾。

Mathlib 已經內建這個結果：

theorem Nat.Prime.infinite : {p : ℕ | Nat.Prime p}.Infinite := by
  exact Nat.prime_infinite

更精確地，Mathlib 提供的 Nat.Prime.infinite 是從「任意有限集合都會遺漏某個質數」 的角度陳述的。我們也可以自己動手證一個局部版本，體會 Euclid 的論證：

-- 給定一個數 n，存在質數大於 n
example (n : ℕ) : ∃ p, Nat.Prime p ∧ n < p := by
  obtain ⟨p, hp, hn⟩ := Nat.exists_infinite_prime n 0
  exact ⟨p, hp, hn⟩

背後的核心引理是： \(n + 1\) 有一個質因數，且該質因數大於 \(n\) 的所有質因數會導出矛盾。 Mathlib 中的 Nat.exists_infinite_prime 就封裝了這條路線。

判斷質數的小工具#

實作上，判斷 \(n\) 是否為質數只需檢查 \(2\) 到 \(\sqrt{n}\) 之間有沒有因數：

/-- 用試除法判斷 n 是否為質數（作為程式，不是證明）。 -/
def isPrimeTrial (n : ℕ) : Bool :=
  if n < 2 then false
  else (2 * 2 ≤ n → ∀ k, 2 ≤ k → k * k ≤ n → n % k ≠ 0) && true

上面的寫法刻意保守：把「沒有小於等於 \(\sqrt{n}\) 的因數」寫成命題，而不是迴圈， 因為在 Lean 中直接寫迴圈還需要證明終止。若要驗證它與 Nat.Prime 一致，可利用 Mathlib 的 Nat.Prime 判定引理：

-- Nat.Prime 的判定：n 是質數 ↔ 沒有 2 ≤ k ≤ √n 的因數
example (n : ℕ) (hn : 2 ≤ n) :
    Nat.Prime n ↔ ∀ k, 2 ≤ k → k ≤ n → ¬ (k ∣ n) := by
  rw [Nat.prime_def_lt_two] <;> sorry -- 完整證明見練習

Mathlib 中實際可用的工具還有：

#check Nat.prime_def_lt_two
#check Nat.Prime.ne_zero
#check Nat.Prime.not_dvd_one
#check Nat.prime_two
#check Nat.prime_three

小結與練習#

本節重點：

  • \(a \mid b\) 定義為 \(\exists k,\ b = a \cdot k\) ，核心引理是 dvd_refl、dvd_trans。
  • Nat.Prime p 定義為 \(2 \le p\) 且「乘積分解必有一邊為 1」。
  • Euclid 論證： \(p_1 \cdots p_k + 1\) 製造新質數；Mathlib 對應 Nat.Prime.infinite。

練習：

  1. 證明：若 \(a \mid b\) 且 \(b \mid a\) ，則 \(a = b\) （提示：Nat.dvd_antisymm）。
  2. 證明：若 \(p\) 是質數且 \(p \mid n \cdot n\) ，則 \(p \mid n\) （提示：先證 \(p \mid n\) 或 \(p \mid n\) ，其實這是 Euclid lemma 的特例，可用 Nat.Prime.dvd_mul）。
  3. 用 decide 檢查 \(5, 7, 11, 13\) 都是質數， \(9, 15, 21\) 不是。
  4. 挑戰：證明對任意 \(n \ge 2\) ，存在嚴格大於 \(n\) 的質數（提示：考慮 \(n! + 1\) ， 用 Nat.factorial 與 Nat.Prime.exists_gt）。
  5. 思考題：Euclid 論證中為什麼 \(p_i \nmid (p_1 \cdots p_k + 1)\) ？ 試在 Lean 中用 Nat.dvd_add_right 或餘數論證表達這件事。