Lean 學習筆記 Day 1 - 畢氏定理

2026.09.07

Lean4 Github：https://github.com/leanprover/lean4
我的 Github：https://github.com/neojou/lean_study
本篇程式：mymathlib
LEAN Community：https://leanprover-community.github.io/
mathlib4：https://github.com/leanprover-community/mathlib4
Lean 4 定理證明（中譯本）：https://www.leanprover.cn/tp-lean-zh/

前篇：Lean 學習筆記 Day 0 - 環境設置 - 2026.09.06
再前篇：Lean 4 從哪裡來：一個證明器決定「自己寫自己」的故事
數學稿（本篇不重述）：當餘弦變成零：一條不繞圈子的畢氏定理證明

底下文章為 Gork AI 所做

Day 0 把衣櫃管理員 elan 和工地主任 lake 請到位了。資料夾會說話，toolchain 釘得住，Hello, world! 也印出來了。接下來最容易犯的錯，是立刻去證明一個「看起來很厲害」的東西，然後在 Infoview 裡跟紅字相處三小時，最後懷疑人生。

所以 Day 1 選一個大家都以為自己早就會的命題：畢氏定理。

\(a^2 + b^2 = c^2\)

國中就背過。問題不在公式本身，而在這句話搬進 Lean 之後，機器到底承認了什麼、又拒絕假裝什麼。數學推導我已經寫在科學筆記那篇：從投影定理出發，用消去得到餘弦定理，再讓直角把餘弦項變成零。那篇文章處理「這條路有沒有循環」。本篇只做一件比較掃興、也比較誠實的事——看同一條路，在 Lean 裡怎麼被寫成機器肯蓋章的稿。

程式在這裡：github.com/neojou/lean_study/tree/main/mymathlib。

先說清楚：Lean 不是自動作文機

Day 0 畫過那張流程圖。AI 可以猜下一步，Lean 只負責不讓你矇混過關。今天沒有請模型代打，但那條分工仍然適用：人負責想清楚假設與結論，Lean 負責檢查每一步的類型、引用、目標是不是真的消失。

這也解釋了為什麼第一個定理不該從「歐幾里得卷一命題 47 全套形式化」開始。那是一棟大樓。我們先蓋一間可以進去躲雨的棚：把紙上已經寫過的代數消去，翻譯成 Lean 看得懂的假設、結構、定理與戰術。

中文教材就用社群在譯的《Lean 4 定理證明》：https://www.leanprover.cn/tp-lean-zh/。原書是 Avigad、de Moura、Kong、Ullrich 的 Theorem Proving in Lean 4。本篇會把程式裡真正用到的指令，對回書裡的章節；不把全書抄一遍。書是地圖，程式才是今天走的那條巷子。

倉庫長什麼樣子

mymathlib 不是單一檔案的作業繳交，而是一個被 lake 管起來的小函式庫。Day 0 建的 my_first_lean_project 比較像打招呼；這裡開始像在擺書架。

lakefile.toml 裡值得先看三件事。

name = "mymathlib"
defaultTargets = ["LinearAlgebra", "Trigonometry", "Pythagorean", "mymathlib"]

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.34.0-rc2"

[[lean_lib]]
name = "Trigonometry"

[[lean_exe]]
name = "mymathlib"
root = "Main"

第一，Mathlib 版本被釘死。這不是潔癖，是求生。Mathlib 走得快，不釘版本，過兩週你的證明可能只是「昨天還是對的」。

第二，函式庫拆成三塊：LinearAlgebra、Trigonometry、Pythagorean。同一條畢氏定理，倉庫裡其實走了兩條路。一條是內積空間：垂直時混合項消失，平方和自然出現。另一條才是本篇主角——投影關係推出餘弦定理，直角時餘弦為零。

第三，Main.lean 只是可執行檔入口，負責印兩句人話。真正的數學不在 main 裡。定理證明專案裡，main 常常只是門房。

import Pythagorean.All

def main : IO Unit := do
  IO.println "Pythagorean theorem verified through real inner-product space theory."
  IO.println "Pythagorean theorem proved using trigonometric functions."

編譯仍是 Day 0 那兩句：

lake build
lake exe mymathlib

第一次拉 Mathlib，記得先 lake exe cache get。否則你會以為自己在證明畢氏定理，其實是在證明家裡的風扇還轉不轉。

三角這條線的檔案

檔案	它答應做的事
`Trigonometry/Projection.lean`	幫長度取一個平行投影、一個垂直投影；順便記下單位圓恆等式。餘弦定理那條主證明不靠這條平方和。
`Trigonometry/CosineLaw.lean`	把三條投影關係收成一個結構，再用消去得到餘弦定理，並取直角特例。
`Trigonometry/Pythagorean.lean`	給直角三角形一個比較好聽的定理名字。內容幾乎是上一檔的 `exact`。
`Trigonometry/All.lean`	雨傘模組。外面只想 `import Trigonometry.All` 時用。

這種切法不是為了看起來專業。是為了讓「假設」和「結論」住在不同房間。形式化最常見的翻車，就是把要證的東西先藏進定義裡，再假裝推了出來。倉庫把兩條路分開，就是在預防自己作弊。

數學稿請去隔壁，這裡只留地圖

科學筆記那篇把幾何說完了，這裡只留方向，避免把同一場消去再演一次：

任意三角形裡，一邊等於另外兩邊在它上面的投影之和。這叫投影定理，只用線段加減與「鄰邊比斜邊」。
三式分別乘上對應邊長，做 \(a^2+b^2-c^2\)，交叉項退場，留下餘弦定理：\(c^2=a^2+b^2-2ab\cos C\)。
\(\angle C=90^\circ\) 時 \(\cos C=0\)，修正項消失，畢氏定理掉出來。

重點是順序：投影 → 餘弦定理 → 直角特例。不是先偷用 \(\sin^2\theta+\cos^2\theta=1\)，再回頭宣稱自己證明了平方和。Loomis 說三角證明不可能，是因為他把三角學定義得太窄；換出發點，門就開了。細節請看當餘弦變成零。

Lean 要做的，是把這張地圖變成「有類型的句子」。

第一句 Lean：假設長什麼樣子

打開 Trigonometry/CosineLaw.lean，頭幾行已經是整份教材的縮影。

import Trigonometry.Projection

/-!
# The cosine law by algebraic elimination
...
-/

structure ProjectionRelations (a b c A B C : ℝ) : Prop where
  side_a : a = b * Real.cos C + c * Real.cos B
  side_b : b = a * Real.cos C + c * Real.cos A
  side_c : c = a * Real.cos B + b * Real.cos A

可以拆成四種語氣。

`import`：先把別人的書架推進來

Lean 檔案不是自動看見全世界。你 import 誰，才能用誰。導入是傳遞的：Trigonometry.Projection 自己 import Mathlib，於是這裡也能寫 Real.cos。對應教材裡「與 Lean 交互」那章講函式庫的部分。

有個小事：這個檔案雖然 import 了 Projection.lean，後面的餘弦定理證明並沒有呼叫 projection_squared_sum。Import 讓你「用得到」，不等於你「用了」。讀程式時要分清楚這兩件事，否則又會被循環論證的幽靈嚇到。

`/-! ... -/`：寫給人看的旁白

模組文件註解不是給編譯器用的。Lean 核對時不理會你的文筆。但它決定半年後的你還認不認得出自己。好的 /-! 不寫心情，寫契約：這個檔案假設什麼、不假設什麼、下一檔會拿它做什麼。

`structure ... : Prop`：把三句話捆成一包假設

這是本篇最值得學的語法之一。教材在「結構與記錄」章會正式講 structure。這裡的用法很樸素：三條投影公式本來就是綁在同一座三角形上的，分開寫成三個獨立假設，後面引用時會像在解繩結。

: Prop 的意思是：這個結構不是一筆資料，而是一個命題。裡面的欄位 side_a、side_b、side_c 都是等式。以後你若有 h : ProjectionRelations a b c A B C，就可以寫 h.side_a 把第一條等式取出來。點號在這裡不是物件導向的時髦，是「打開這包假設」。

參數全是 ℝ。Lean 此時並沒有先檢查 \(a,b,c\) 是否能圍成三角形、角是否為正、邊是否為正。它只準備討論「若這三條實數等式成立，則後面那條平方關係也成立」。幾何直觀被收成假設，代數消去才是定理本體。這不是偷懶，是分工。歐氏幾何的投影事實，可以之後再形式化；今天先保證消去本身沒寫錯。

`Real.cos`：我們站在誰的肩膀上

這裡的餘弦不是我們自己用「鄰邊比斜邊」從零定義出來的，而是 Mathlib 分析庫裡的 Real.cos。直角時會用到的 Real.cos_pi_div_two，也是庫定理。形式化常常是這種拼圖：幾何故事在註解裡，分析對象在庫裡，中間那截消去才是你親手寫的。

有人會問：那還算不算「用三角證畢氏」？算。因為循環與否，關鍵不在符號叫不叫 cos，而在你有沒有把 \(\sin^2+\cos^2=1\) 或直角平方和預先塞進這條消去。這個檔案沒有。

定理怎麼開口

theorem cosine_law_from_projections
    (a b c A B C : ℝ) (h : ProjectionRelations a b c A B C) :
    c ^ 2 = a ^ 2 + b ^ 2 - 2 * a * b * Real.cos C := by
  have ha := congrArg (fun x : ℝ => a * x) h.side_a
  have hb := congrArg (fun x : ℝ => b * x) h.side_b
  have hc := congrArg (fun x : ℝ => c * x) h.side_c
  have hcancel : a ^ 2 + b ^ 2 - c ^ 2 =
      2 * a * b * Real.cos C := by
    nlinarith [ha, hb, hc]
  nlinarith [hcancel]

這一段幾乎就是《定理證明》前幾章的現場示範。

`theorem` 與冒號

名字、參數、冒號、結論。讀成中文就是：

對任意實數 \(a,b,c,A,B,C\)，若它們滿足投影關係 \(h\)，則餘弦定理成立。

教材「命題與證明」章會強調一件讓初學者不舒服的事：在 Lean 裡，命題也是類型，證明是這個類型的項。你寫 theorem foo : P := by ...，就是在構造一個類型為 \(P\) 的東西。機器不在乎你是否「覺得顯然」，它只問這個項構不構得出來。

`:= by`：從寫項切到開戰術

等號右邊可以直接給一個證明項，像寫函數一樣。但人通常受不了那種精細度，於是改寫 by，進入戰術模式。戰術是給人用的遙控器：你說「改寫這個」「引用那個」「把目標丟給線性算術」，Lean 在幕後組出真正的證明項。

Infoview 此時最重要。目標寫在 ⊢ 後面，假設寫在上面。每執行一句戰術，目標應該變短、變少，或至少變得比較像人話。若目標愈變愈怪，多半不是 Lean 壞了，是你走錯巷。

對應教材：戰術那一章。

`have`：先在邊上放一塊積木

have ha := ... 的意思是：我先證明一個中間事實，取名叫 ha，稍後再用。紙上證明寫「令……」「於是……」，Lean 裡常常就是一串 have。

這裡三個 have 對應數學稿的「兩邊乘上各自的邊長」。Lean 不懂得你心中的「兩邊同乘」，它需要一個函數去作用在等式兩端。congrArg f h 說的是：若 \(h\) 是 \(x=y\)，則 \(f(x)=f(y)\)。於是

congrArg (fun x : ℝ => a * x) h.side_a

就是把

\[ a = b\cos C + c\cos B \]

變成

\[ a\cdot a = a(b\cos C + c\cos B). \]

你在紙上用拇指按住「乘 \(a\)」這一步，機器要求你把拇指也寫下來。這就是形式化的稅。稅很煩，但換來一件好事：這一步再也無法含糊。

fun x : ℝ => a * x 是匿名函數。教材在依值類型論與命題章都會碰到它。讀法很普通：「那個把 \(x\) 送去乘 \(a\) 的規則」。

`nlinarith`：請一位會計進場

三個乘完的等式到手之後，紙上要做 \(a^2+b^2-c^2\)，看哪些交叉項互相鞠躬下台。這段在 Lean 裡交給 nlinarith。

它不是魔法，是 Mathlib 的非線性算術戰術：在實數環上，對多項式等式與不等式做有限的推敲。你把可以使用的等式放進方括號 [ha, hb, hc]，等於告訴它：「帳簿只准用這幾頁。」

兩次 nlinarith 拆開寫，是為了讓中間結果 hcancel 可見。也可以擠成一句，但初學時可見比較重要。證明不是越短越好，是下一步還認不認得出來。

有人會覺得把消去丟給戰術，好像自己沒證。相反：你已經把幾何收縮成三條等式，把乘法寫成 congrArg；剩下的環運算本來就該讓機器做。人負責方向，機器負責不抄錯符號。這和 Day 0 說的「猜、查、改」是同一種禮貌——人可以想得瀟灑，帳必須結得刻薄。

直角那一下：`simpa` 與 `using`

theorem cosine_law_right_angle
    (a b c A B : ℝ)
    (h : ProjectionRelations a b c A B (Real.pi / 2)) :
    c ^ 2 = a ^ 2 + b ^ 2 := by
  simpa [Real.cos_pi_div_two] using
    (cosine_law_from_projections a b c A B (Real.pi / 2) h)

這是整條路最像「把故事說完」的一句。

ProjectionRelations a b c A B (Real.pi / 2) 把角 \(C\) 直接釘成 \(\pi/2\)。注意 Lean 用弧度。數學稿寫 \(90^\circ\)，庫裡寫 Real.pi / 2。單位換了，邏輯沒換。

using 後面是已經證過的餘弦定理，只是把那個一般的 \(C\) 代入直角。simpa [Real.cos_pi_div_two] 則說：請順便用「直角餘弦為零」這條庫引理簡化。簡化完，- 2ab\cos C 消失，目標變成畢氏定理。

simpa 可以想成「simp 完再 assumption / 收尾」的合成拳。simp 本身是教材戰術章的主角之一：依照標了 [simp] 的引理，把表達式往較簡的形狀改寫。這裡我們手動把 Real.cos_pi_div_two 放進方括號，等於指定今晚只准用這一把刀，避免 simp 興致一來把整張桌子拆掉。

然後是最後一個小檔案：

theorem trigonometric_pythagorean
    (a b c A B : ℝ)
    (h : ProjectionRelations a b c A B (Real.pi / 2)) :
    c ^ 2 = a ^ 2 + b ^ 2 := by
  exact cosine_law_right_angle a b c A B h

exact 的意思是：我手上這個東西，類型剛好就是目標，請收工。沒有新數學。有的只是命名。形式化專案裡，這種「幾乎只是別名」的定理非常常見。人讀書靠章節標題，機器核對靠名字。給直角特例一個比較像口語的名字，之後引用時比較不像在念檔案路徑。

旁邊那條內積路，也值得看一眼

同一倉庫的 LinearAlgebra/InnerProduct.lean 用另一種方式講同一句話：若 \(\langle u,v\rangle=0\)，則

\[ \|u+v\|^2 = \|u\|^2 + \|v\|^2. \]

證明幾乎是把內積對加法展開，再用對稱把交叉項寫成兩倍，然後讓它等於零。戰術是 rw、intro、dsimp、ring。和三角那條比，少了餘弦，多了向量。

Pythagorean/Classical.lean 再把抽象定理裝回平面座標：點就是 \(\mathbb{R}\times\mathbb{R}\)，直角三角形是兩條互相正交的邊向量，斜邊是它們的和。最後用 simpa using 把抽象結果接上古典距離。

為什麼同一個倉庫要養兩種證明？因為「畢氏定理」這五個字其實含糊。它有時是三角形三邊，有時是向量正交，有時是座標裡的距離公式。Lean 逼你把含糊拆開。拆開以後才知道：座標距離若一開始就定義成 \(\sqrt{x^2+y^2}\)，那你不是在證畢氏，是在把定義念出來。這個倉庫故意讓距離走內積，讓三角走投影消去，兩邊都不把結論藏進定義。

Day 1 主線仍是三角。內積那條留給之後想寫線性代數時再展開。現在知道書架上有它，就夠了。

把今天用到的指令對回教材

若你打開 Lean 4 定理證明不知道先讀哪，可以用這張對照表當書籤。不必依序讀完才准寫程式；比較有效的是：寫到哪個指令，再回頭看那一節。

你在程式裡看見	它在幹什麼	建議對照
`import`	引入已編譯模組	與 Lean 交互／使用庫
`def` / `noncomputable def`	定義一個對象；後者允許用到古典選擇或分析裡不可計算的部分	依值類型論、定義
`structure`	把一組欄位捆成定義或命題	結構與記錄
`theorem ... : P := by`	宣告命題並進入戰術模式	命題與證明、戰術
`have`	引入中間命題	戰術：have / let / show
`congrArg`	函數作用在等式兩端	量詞與等式
`rw` / `dsimp`	依等式或定義改寫	戰術：rewrite、simp
`simpa ... using`	簡化後接上已有證明	戰術：simp
`exact`	手上的項就是目標	戰術開頭幾節
`nlinarith` / `ring`	把環上的帳交給自動化	戰術章末、Mathlib 慣例
`intro`	打開 \(\forall\) 或蘊含	戰術、量詞

另外三個今天沒寫進主證明、但你開 Infoview 一定會碰到的指令：

#check：問 Lean「這東西是什麼類型」。
#print：把定義或定理的本體印出來。
sorry：暫時承認這裡有個洞。可以編譯，不能算證完。它是便利貼，不是獎狀。

自然數遊戲仍然值得當手指熱身：NNG4。那邊逼你把 rw、induction、exact 練成肌肉記憶。等肌肉有了，再回來看 nlinarith，才不會以為所有證明都該丟給自動化。

這份證明「證到哪裡為止」

寫形式化最容易膨脹的，是自我感覺。所以把邊界講白。

機器確實核對了的：

若三條投影等式成立，則餘弦定理那條代數關係成立。
若其中一個角是 \(\pi/2\)，且 Mathlib 的 Real.cos (\pi/2)=0 可用，則平方和成立。
中間每一步的類型與等式改寫合法。

機器今天還沒被要求核對的：

平面幾何裡，從頂點作高後，底邊為何等於兩段投影之和。
餘弦作為「鄰邊／斜邊」與分析庫裡 Real.cos 的對應。
邊長為正、可構成三角形、角的範圍。

換句話說：這是「消去這段代數」的核可本，不是《幾何原本》的數位重建。這樣寫有一個好處——循環論證變得看得見。若有人把 projection_squared_sum 那條 \(\sin^2+\cos^2=1\) 拿來推畢氏，檔案依賴會立刻露出馬腳。今天這條主證明沒走那扇門。

形式化的價值常常不在「終於連國中數學也進了電腦」，而在把「我以為沒有縫」的地方畫出縫來。

以後要繼續寫 Lean，我會怎麼做

給自己的備忘，也給之後可能跟著做的人。不是教條，是踩過紅字之後比較不想再踩的幾件事。

1. 先寫命題，再寫證明。
定理簽名比戰術重要。假設是什麼、結論是什麼、哪些對象活在哪個類型裡，先用 sorry 讓它通過編譯。目標清楚了，戰術才有地方可以砍。反過來先堆 rw，多半是在濃霧裡揮劍。

2. 假設用結構收起來，不要讓參數列長到像購物清單。
三條投影關係合成 ProjectionRelations，後面引用才像人話。以後若做正弦定理、面積公式，也可以各收成一包。結構是給命題用的行李箱。

3. 定義裡不准偷藏結論。
距離不要一開始就寫成畢氏公式，再宣布自己證明了畢氏。直角三角形不要定義成「三邊滿足平方和的東西」。讓定義薄，讓定理厚。這是這個倉庫最想示範的品味。

4. 一個檔案只講一個故事。
投影、餘弦、直角特例、古典平面、抽象內積，分開住。上面再用 All.lean 當門口。之後要改其中一條路，不會把另一條路的註解一起嚇醒。

5. 先搜 Mathlib，再發明輪子。
Real.cos、Real.cos_pi_div_two、nlinarith、ring 都已經在。重複發明餘弦，通常不是創見，是還沒學會查。VS Code 裡把游標放在名字上，跳到定義，比重新打一遍有用。

6. 讓證明讀起來像那篇數學稿。
數學稿寫「兩邊乘邊長，再做 \(a^2+b^2-c^2\)」；Lean 就用三個 have 加一個 hcancel。名字對得上文章，以後除錯才找得到自己。形式化不是把中文翻譯成火星文，是把中文收成機器也認的中文。

7. 自動化戰術要關在籠子裡用。
nlinarith、simp、aesop 都很能打，但也都會在你沒注意時用到你不想用的引理。把用得到的等式顯式列在方括號裡。成功時你才說得出「它靠的是哪幾頁帳簿」。

8. 紅字是教材，不是羞辱。
Infoview 的錯誤訊息難讀，但比「我總覺得哪裡不對」有用。讀紅字的順序通常是：目標是什麼、它以為你給的類型是什麼、哪一個參數對不上。Day 0 說的迴路在這裡落地：猜一句戰術，讓 Lean 查，再改。

9. 版本繼續釘死，快取繼續用。
lean-toolchain 與 lakefile.toml 的 rev 不要隨手改。改之前先問：是數學需要新引理，還是只是手癢。

10. 下一題選「比畢氏稍硬一點、但假設仍然收得住」的。
例如：把投影關係從「作為假設」推進到「從幾何模型推導」；或者把正弦定理用同樣風格寫成結構加消去；或者沿內積那條線把柯西－施瓦茨寫出來。不要下一篇就攻克費馬最後定理。機器很有耐心，人的週末沒有那麼多。

收工

Day 0 證明的是環境裝得起來。Day 1 證明的是：一句國中公式，可以在 Lean 裡被寫成「假設清楚、消去可核對、直角只是特例」的小函式庫。數學故事在那篇餘弦變成零；這裡多出來的，是機器肯蓋的章，以及我們終於被迫承認自己還沒蓋的那些章。

畢氏定理被證明過幾百次。多一次 Lean 版，不會讓它更真。真的改變的是寫證明的人：你開始害怕「顯然」，開始喜歡把假設印在結構裡，開始能接受會計進場把交叉項對掉。

明天若還要寫，就讓書架上再多一本小書。不必一次蓋成圖書館。

程式仍在：mymathlib。
語法地圖仍在：Lean 4 定理證明。

搜尋此網誌

Neoの世界へようこそ

精選文章

Have you ever had a dream that you were so sure was real