最近在沉迷數學證明
Lean 是一個可以拿來寫數學證明的語言。開發者架設了一個 網站，把數學證明變成一關一關的遊戲，讓使用者可以透過遊戲學習 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 到底在提示什麼。