add lean lang post

content/posts/2026-02-18_lean_lang.md

@@ -0,0 +1,107 @@
+---
+title: "Lean Language Experience"
+date: 2026-02-18
+draft: false
+---
+
+![](images/lean.png)
+
+{{< translation type="machine" from="Chinese" />}}
+
+I was obsessed with math proving recently.
+
+Lean is a language you can use to write mathematical proofs. The developers set up a [website](https://adam.math.hhu.de/#/g/leanprover-community/nng4) that turns mathematical proofs into a level-by-level game, letting users learn how to use the Lean language through gameplay.
+
+I first heard about this language around the end of 2024, when Terence Tao mentioned using AI to assist with mathematical proofs, with Lean playing a central role. About half a year ago I came across the game website, but I think I got through the first or second command and then just stopped. Not sure if I was tired that day, or the server went down, or I was busy with something else — whatever it was, I couldn't make progress and quickly got distracted and gave up.
+
+I learned from friends from my recent Japan trip that cryptographers in Japan are trying to describe the mathematics of cryptography using Lean. So last week I thought of the game again.
+
+This time, once I started it up, I just kept going level by level. I cleared all the natural numbers content built from the Peano axioms.
+
+(Strictly speaking, it's not a full clear. One level has Fermat's Last Theorem in it. The level description says the shortest known human proof requires one million lines of Lean code. Actually finishing that one might require going to get a math degree.)
+
+After natural numbers, there are chapters on set theory, real analysis, linear algebra, and more. Right now I'm slowly making my way through set theory.
+
+## What does it feel like to write proofs in Lean?
+
+The second level of the tutorial game is a pretty good illustration of what writing a proof in code feels like. The problem in plain language is: "If x and y are natural numbers, and y = x + 7, then 2y = 2(x + 7)."
+
+In the game interface, this problem gets translated into a "goal" and some "hypotheses."
+
+The **goal** is to prove:
+
+`2 × y = 2 × (x + 7)`
+
+And you have certain **hypotheses** — things that are assumed to be true:
+
+`h: y = x + 7`
+
+Then the user types `rw[h]` into the interactive interface. This command says we want to rewrite the expression in the goal by substituting in the existing hypothesis h. Lean understands that this means replacing every occurrence of y with x + 7.
+
+After executing the command, the goal updates to:
+
+`2 × (x + 7) = 2 × (x + 7)`
+
+When you see that both sides of the equation are identical, you type `rfl` (short for reflexivity — I didn't really know what that meant either), and the game interface shows that the proof is complete.
+
+Each time you clear a level, you might unlock new theorems that get added to your toolbox, available to use in future levels.
+
+## How has using Lean changed how I feel about math?
+
+I think the mystery of mathematics has disappeared.
+
+Even though I've spent a fair amount of my life on mathematics, my training made me a *consumer* of math, not a *producer*.
+
+Here's how I define it: consumers take mathematical formulas and plug in actual numbers to apply them. Producers are responsible for generating the formulas and proving that using them won't blow up in your face.
+
+Consumers don't really worry about proofs.
+
+I'd typically encounter mathematical formulas in textbooks or papers, sometimes with a proof attached. But whether handwritten, printed, or beautifully typeset in LaTeX, they're designed to be digested by a human brain. The reader needs a certain level of mathematical capital to make sense of the formulas and proofs.
+
+Whether a paper is correct gets checked by a group of capable reviewers using their human brains.
+
+For the consumer, math is still magic.
+
+Under Lean, a proof gets broken down into a series of small actions: substituting symbols, applying an already-proven theorem, invoking mathematical induction, using proof by contradiction.
+
+Now when I hear the words "mathematical proof," my gut reaction is no longer "magic" — it's "business logic."
+
+I feel like I've seen Adam Smith's pin factory.
+
+Those pen-and-paper manipulations become computer operations. Verifying mathematical correctness is no longer repetitive human labor — it's automatic execution by a computer in seconds.
+
+The straight-line conclusion I'm drawing is that everywhere LaTeX currently appears, it will eventually be replaced by something like Lean code.
+
+## Why now?
+
+The history of automating mathematical proofs must go back quite a while. I'm only just getting into this, so I don't know what happened in the past or what challenges had to be overcome to arrive at something like Lean.
+
+I've heard the names Isabelle and Coq before. A senior colleague once took a whole team to study Coq in order to develop a better zero-knowledge proof language. All I know is that when they were working through some exercises, only one person on the entire team — the youngest — could solve them. I'm not sure if the language was hard to use or if the exercises were just genuinely difficult.
+
+It's hard to feel how good or bad a developer experience is without comparing it to other languages and all the hard work behind the scenes. But so far, Lean has been extremely smooth and remarkably intelligent to use. I've barely been blocked by any language-specific obstacles.
+
+## Thoughts on proof after using Lean
+
+I used to hate mathematical induction most of all when studying math. Beyond telling you a conclusion is true, induction doesn't really give you any insight. So why spend the brainpower working through a proof? It felt like proving for the sake of proving.
+
+And yet, playing Lean's game is literally proving for the sake of proving. The number of moves that can actually advance your goal is quite limited — if you can use induction, you use it; if you can breakdown a definition, you break it down.
+
+Let me add a bit about how Lean handles mathematical induction, because it's actually pretty interesting. When you invoke induction, you specify which variable to apply it to. Lean moves your current goal to a to-do list to be handled later. Your new immediate goal becomes proving the case where n = 0. After n = 0 is proven, your current goal becomes proving the n = k + 1 case, with the "induction hypothesis" introduced as an available assumption. Once both sides are proven, it returns to the original goal.
+
+## Experiences getting stuck
+
+In the natural numbers chapters, most problems were about slowly feeling your way through. If a command could do something, you were probably one step closer to finishing the proof. Playing those levels, I barely paid attention to what I was actually proving mathematically.
+
+The problems are usually stated in fairly abstract mathematical terms — like 2 + 2 = 4. In the Peano world, only the concepts of 0 and successor numbers exist. So you first have to decompose 2 and 4 into their successor definitions — 4 is the successor of 3, 3 is the successor of 2. Then you apply the available operations on successors (like how they interact with addition) to complete the proof.
+
+So the brainless strategy is: see an abstract symbol, find its definition and break it down. Keep breaking until you can't anymore, then figure out how to reassemble.
+
+Some levels require more strategy. In the set theory chapters, some proofs require you to prove that some variable *exists* which satisfies certain conditions. In Lean, that means producing a concrete example and checking whether it passes those conditions.
+
+For the player, picking the right example sends you to heaven. Picking the wrong one means no matter how hard you try, the proof won't go through.
+
+This is when you actually need some understanding of the mathematical problem to pick the right example.
+
+The natural numbers world was a two-day binge, but the set theory world had levels where I was stuck for a full day.
+
+For those stuck-for-a-day moments, I'd already snuck a peek at AI, then looked at discussions on the official Zulip forum, and had to work things out by hand before I finally understood. That handwriting step was what it took to understand what a certain symbol meant in terms of proof strategy — and only then could I judge whether the AI was making things up, and what the spoiler hints on the forum were actually pointing at.

content/posts/2026-02-18_lean_lang.zh-TW.md

@@ -0,0 +1,110 @@
+---
+title: "Lean 語言體驗"
+date: 2026-02-18
+draft: false
+images:
+- images/lean.png
+---
+
+![](images/lean.png)
+
+最近在沉迷數學證明
+
+Lean 是一個可以拿來寫數學證明的語言。開發者架設了一個 [網站](https://adam.math.hhu.de/#/g/leanprover-community/nng4)，把數學證明變成一關一關的遊戲，讓使用者可以透過遊戲學習 Lean 語言的用法。
+
+我應該是在 2024 年底聽過這個語言，那時聽到陶哲軒說要用 AI 輔助數學證明，其中就要倚賴 Lean 語言。大概在半年以前看到那個遊戲網站，但我好像做了第一個還是第二個指令就停下來了。不知道是那天精神不好，還是伺服器斷線，還是在忙其他事，反正就是無法前進遊戲，一下子就分心放棄遊戲了。
+
+最近聽了日本的朋友說他們的密碼學家都在嘗試用 Lean 描述密碼學中的數學。所以上週我又想起了這個遊戲。
+
+這次再開起來之後，一下子就一關一關的玩下去。把從皮亞諾公設建構的自然數玩完了。
+
+（嚴格來說，應該不算全破關。有一關放了費馬最後定理。關卡的說明寫說人類已知最簡短的證明需要百萬行的 Lean 程式碼。要全破可能真的要去念數學系）
+
+自然數玩完之後，還有集合論、實分析、線性代數等關卡。現在在集合論慢慢前進中。
+
+## 使用 Lean 語言寫證明的感覺是什麼呢？
+
+教學遊戲的第二關蠻適合描述用程式寫證明的過程是什麼。題目用文字描述是「如果 x 和 y 是自然數，且 y=x+7，則 2y=2(x+7)」
+
+在遊戲的界面中，這個問題會被轉換為「目標」和「假設」。
+
+「目標」是證明
+
+2 × y = 2 × (x+7)
+
+然後你有若干「假設」，假設的意思就是被假設是對的。
+
+h: y = x + 7
+
+接下來使用者在互動式的界面鍵入 `rw[h]` 指令。這個指令表達我們想把目標的式子重寫（rw 是 rewrite 的縮寫），用帶入現有的假設 h 。Lean 會知道說這要把變數 y 都代換成 x + 7
+
+指令執行之後，目標的式子會更新。變成
+
+2 × (x+7) = 2 × (x+7)
+
+看到等號左右兩邊的符號一樣時，再鍵入 `rfl` 指令（reflexity 的縮寫，我也不知道是什麼意思），遊戲界面就會呈現這個證明完成了。
+
+每次過關，可能可以解鎖新的定理，加到工具箱裡面，在未來的關卡中使用。
+
+## 用了 Lean 語言之後對數學的感受是什麼呢？
+
+覺得數學的神秘感消失了吧。
+
+雖然人生花了不少時間在數學上，但我的訓練就是一個數學的消費者，不是生產者。
+
+我的定義是這樣：消費者拿數學公式，帶實際的數字去做應用。生產者負責生產公式，並證明公式用了不會出事。
+
+消費者不太管證明。
+
+我通常會在課本或論文看到數學公式，公式旁邊可能會附上證明。
+
+但這公式或證明不管是手寫的、印刷的、還是打成美麗的 latex 排版，他們是被預期用人腦去消化。讀者腦袋要具備某種程度的數學資本，才能讀懂這些公式和證明。
+
+論文有沒有寫對，是一群有能力的 reviewers 用人腦檢查有沒有錯誤。
+
+對消費者而言，數學還是魔法。
+
+在 Lean 語言之下，證明被拆解成一系列小小的動作：符號代換、套用某個已證明的定理、使出數學歸納法、使出反證法。
+
+聽到數學證明這個詞之後，腦袋的直覺反應不再是「魔法」，而是「業務邏輯」。
+
+我覺得我看到了亞當斯密的別針工廠。
+
+那些紙筆的動作，變成電腦的運算。驗證數學的正確，不再是人力重複的勞動，而是電腦數秒間的自動執行。
+
+直線的思考是以後應該有 latex 出現的地方，全部會變成類似 Lean 語言的程式碼。
+
+## 為什麼是現在？
+
+要把數學證明自動化的歷史應該很早。只是我現在才剛接觸，不知道過去發生什麼事，也不知道要變成 Lean 語言這樣要經歷什麼樣的挑戰。
+
+我有聽過 Isabelle, coq 這些名字。之前資深同事為了開發一套更好的零知識證明語言，帶了一團人去學 coq 。我只知道他們在研究某個習題時，全員只有一位最年輕的同事解得出來。不知道是語言難用，還是習題本來就難。
+
+雖然開發者體驗的好和背後所需要的苦工沒比較過其他語言是不太容易感受的。但目前為止 Lean 用起來非常流暢，非常智慧。幾乎沒有被某種語言特定的障礙卡過。
+
+## 用了 Lean 之後對證明的感想
+
+以前學數學最討厭數學歸納法了。除了告訴你一個結論是對的之外，數學歸納法根本沒提供什麼洞見。那為什麼要花腦漿導證明？簡直是為了證明而證明。
+
+然而玩 Lean 的遊戲就是為了證明而證明。能夠推進目標可行的動作其實不多，數學歸納法能用就用，能歸就歸。
+
+補充一下 Lean 怎麼處理數學歸納法，這蠻有趣的。使出數學歸納法時，要指定對哪個變數使用，。 Lean 會把你當下的目標搬到代辦事項，後面再來處理。新的當下目標變成證明 n=0 的情況。然後在 n=0 得證之後，當下目標變為證 n=k+1的情況 ，並引入 「歸納法假說 induction hypothesis」。兩邊都證完之後就會回到原本的目標了。
+
+## 卡關的經驗
+
+在自然數的關卡裡，大部分的題目都是慢慢摸索找路。只要某個指令可以作用，那離完成證明大概就更近一步了。在玩這類的關卡時，我好像都沒有在管題目是要證什麼數學。
+
+通常題目都會是以比較抽象的數學描述，例如 2+2 = 4 。在皮亞諾的世界裡，只有 0 和 後繼數 的觀念。因此必須先把 2 和 4 拆解成後繼數的定義，例如 4 是 3 的後繼數，3 是 2 的後繼數。然後再套用後繼數相關可行的操作方式（例如可以和加法組合），去完成證明。
+
+因此無腦的證明策略就是看到抽象的符號，找定義把它拆小。拆到不能再拆時，再想辦法組合上去。
+
+有些關卡就比較需要策略。在集合論的關卡，有些證明需要證明「存在」某個變數，其符合某些條件。在 Lean 語言中，就是舉一個例子，並檢查是否能通過那個條件。
+
+對玩家來說，舉對例子就是上天堂。舉錯例子當然怎麼證都不會證成功。
+
+這時候，玩家就需要對數學題目有些理解，才能正確舉例。
+
+自然數的世界是兩天 binge 玩完，但集合論世界就有幾關是卡了一天。
+
+卡一天的就是已經偷問了一下 AI ，然後再看了一下官方 Zulip 論壇上面的討論，手寫了一下才參透。
+手寫那一步才理解某個符號在證明策略上的意義，才看懂 AI 有沒有亂講，和論壇上的 Spoiler 到底在提示什麼。