1.1 數學證明的兩難#

本節目標#

• 認識「讀懂證明」與「親手寫出證明」之間的巨大落差
• 理解人類閱卷的主觀性與不精確之處
• 體會「找證明難、查證明易」的不對稱性
• 了解為什麼數學需要一個「機器裁判」

開場：一個看起來沒問題的證明#

先看一個大一新生很常寫的「證明」。

題目：設 \(a\) 、 \(b\) 為實數，證明：若 \(a + b = 0\) ，則 \(a = b\) 。

學生的證明： 因為 \(a + b = 0\) ，顯然可得 \(a = b\) 。得證。

你覺得這個證明對嗎？先別急著往下看，思考十秒。

答案是：命題本身是錯的。取 \(a = 1\) 、 \(b = -1\) ，則 \(a + b = 0\) ，但 \(a \neq b\) 。

這就是數學證明的第一個兩難：有時候連「題目對不對」都需要證明才知道。學生不是證錯，而是證了一個假命題——而且他寫「顯然可得」的語氣，和教科書裡寫「顯然可得」的語氣一模一樣。

再看一個稍微進階的版本。命題是對的，但證明有漏洞：

題目：設 \(a\) 、 \(b\) 為實數，證明：若 \(a + b = 0\) ，則 \(a^2 = b^2\) 。

學生的證明： 由 \(a + b = 0\) 移項得 \(a = -b\) ，兩邊平方得 \(a^2 = (-b)^2 = b^2\) 。得證。

這次命題是真的，證明也大致正確。但如果這是考卷，閱卷老師可能會問：

• 「移項」是什麼性質？你用到了實數的加法反元素存在性，有引以為據嗎？
• 「兩邊平方」是合法操作嗎？為什麼平方不會破壞等式？

在國中，這些問題的答案是「因為老師說可以」。但在大學數學裡，我們要追問到公理層級：實數是一個完備有序體，每一個步驟都必須是體公理或已證明的定理。

教科書的「顯然可得」與考卷上的扣分#

打開任何一本數學教科書，你會看到這些句子：

• 「顯然可得 \(x \leq y\) 」
• 「由簡單的計算可知……」
• 「證明留給讀者（習題 3.2）」
• 「此處省略與前例類似的討論」

教科書寫「顯然」，是因為作者假設讀者已經具備補完細節的能力。問題是——你怎麼知道你具備了？

考卷上的評分標準大致是這樣運作的：

同一份證明，不同老師改，可能差五分到二十分。這不是老師不專業，而是自然語言的證明本來就沒有精確的裁判標準。

證明為什麼需要一個機器裁判#

想想其他領域怎麼解決「裁判不公」的問題：

• 跑步：用碼表和終點攝影，不用目測。
• 體操：有明確的動作難度表與扣分表。
• 國際象棋：規則由程式完全確定，電腦可以判定每一手是否合法。

數學呢？數學的裁判是「數學社群的共識」，這個共識靠同儕審查維持。同儕審查很有效，但很慢：一份論文的證明可能被審查數月甚至數年，而且歷史上不斷出現「已發表但後來被發現有錯」的證明。

如果有一個裁判，它：

1. 從不疲倦——檢查一百萬行證明也不會不耐煩；
2. 從不客套——不會因為你字跡工整而放水；
3. 絕對精確——每一步要麼符合規則，要麼不符合，沒有中間地帶；
4. 完全公開——規則就是一套程式語言的語法，任何人都能檢驗裁判本身。

這個裁判就是證明助理（proof assistant），本書使用的版本叫 Lean。

在 Lean 的世界裡，你的證明要麼被電腦接受，要麼被拒絕，沒有「老師心情」這個變數。這不是要取代人類數學家——找證明仍然需要人類的洞察力——而是把「查證明」這件機械化的工作交給機器。

找證明難、查證明易的不對稱性#

數學中最深刻的不對稱之一：

flowchart LR
    A["找證明<br/>（可能花幾百年）"] --> B["證明寫成文字"]
    B --> C["查證明<br/>（機械式逐步檢查）"]
    C --> D["接受 / 拒絕<br/>（二元判定）"]

費馬在 1637 年於書頁邊寫下「我發現了一個絕妙的證明，可惜這裡空白太窄寫不下」，直到 1994 年 Wiles 才給出完整證明——找了三百五十七年。

但如果費馬當年把他的「絕妙證明」寫下來（假設他真的有），檢查它的難度是多少？一個受過訓練的數學家可能幾天就能逐行檢查完。而如果證明是寫給 Lean 看的，Lean 檢查它只需要幾秒鐘，而且結論百分之百可靠。

這個不對稱性正是本書的教學策略基礎：

• 你負責「找」——思考、嘗試、失敗、再嘗試，這是學數學的核心。
• Lean 負責「查」——它不給你提示（大部分時候），但它絕不讓任何錯誤過關。

學生證明常見錯誤清單#

在進入 Lean 之前，先看看人類閱卷中最常見的錯誤類型。這些錯誤在 Lean 中全部會被攔下來：

1. 循環論證：用結論證結論。Lean 中如果你引用的引理還沒證，就必須用 sorry 標記，瞞不過去。
2. 假命題當真：如開場的 \(a+b=0 \Rightarrow a=b\) 。Lean 中你要先寫出命題，寫不出證明就會一直卡住，這本身就是在提醒你。
3. 漏掉邊界情況：忘記 \(x = 0\) 的情形。Lean 的分類討論（rcases、by_cases）會強制你處理所有情況。
4. 量詞方向搞反：把「存在 \(\varepsilon > 0\) 對所有 \(x\) 」寫成「對所有 \(x\) 存在 \(\varepsilon > 0\) 」。Lean 中 ∀ 和 ∃ 的操作順序完全不同，搞反了寫不出來。
5. 非法操作：兩邊除以可能為零的量。Lean 中除法相關引理都帶有 \(x \neq 0\) 的前提，你必須先補上。

一個可以在 Lean 裡體驗的例子#

你還不需要懂語法，只要感受一下「機器裁判」的感覺。以下是開場那個假命題在 Lean 中的樣子：

-- 這個命題是假的，所以不可能證出來
example : ∀ a b : ℝ, a + b = 0 → a = b := by
  intro a b h
  -- 卡在這裡：無論怎麼寫，Lean 都不讓你過關
  sorry -- 這只是暫時標記，Lean 會警告你

-- 而它的「反例」可以嚴格寫出來：
example : ¬ ∀ a b : ℝ, a + b = 0 → a = b := by
  intro h
  have h1 := h 1 (-1) (by norm_num)
  -- h1 : 1 = -1，這顯然矛盾
  norm_num at h1

第二段程式碼，Lean 會接受。它代表：「我可以嚴格證明那個假命題是假的」。人類閱卷老師可能會因為你沒寫清楚 \(1 + (-1) = 0\) 而扣分，但 Lean 不會——它連 \(1 + (-1) = 0\) 都幫你驗證過了（norm_num 那一行）。

小結與練習#

本節重點#

1. 教科書的「顯然可得」隱藏了大量細節，人類閱卷對「寫多細」沒有客觀標準。
2. 「找證明難、查證明易」的不對稱性，使得把「查」交給機器是合理分工。
3. 證明助理提供絕對精確、永不疲倦的機器裁判。
4. 常見的證明錯誤（循環論證、假命題、漏邊界、量詞搞反）在 Lean 中都會被攔截。

練習#

1. 判斷下列命題的真假，並各寫出證明或反例（用紙筆即可）：
2. 若 \(a + b = 0\) ，則 \(a = -b\) 。
3. 若 \(a^2 = b^2\) ，則 \(a = b\) 。
4. 若 \(a b = 0\) ，則 \(a = 0\) 或 \(b = 0\) 。
5. 找出你以前學過的一份數學證明（課本或筆記皆可），列出其中所有「顯然可得」或被跳過的步驟。你能在兩分鐘內補完每一個嗎？
6. 想一個「人類裁判 vs 機器裁判」的日常例子（例如：書法比賽 vs 珠算檢定），說明兩者各自的優劣。
7. （挑戰）費馬最後定理敘述為：當整數 \(n \geq 3\) 時， \(x^n + y^n = z^n\) 沒有正整數解。為什麼「檢查 Wiles 的證明」比「重新發現它」容易得多？用「找難查易」的不對稱性說明。

下一節，我們正式介紹 Lean 這個工具。