Lean 學習筆記 Day 0 - 環境設置 - 2026.09.06
Lean4 的 Github : https://github.com/leanprover/lean4
我的 Github : https://github.com/neojou/lean_study
LEAN Community: https://leanprover-community.github.io/
這個網站也不錯: https://lean4.dev/
mathlib4 : https://github.com/leanprover-community/mathlib4
LEAN 遊戲服務器 - https://adam.math.hhu.de/
--
前篇：Lean 4 從哪裡來：一個證明器決定「自己寫自己」的故事
--
最近看到這篇文章
以及
The Proof in the Code 讀後心得：當證明開始「編譯」
對 Lean 產生了興趣;
--
關於 機器證明, 我讓 Grok AI 做了一張流程圖, 和寫了底下這段 ：
AI Theorem Proving
機器在證什麼：AI Theorem Proving 的核心其實很短
AI 定理證明的核心，不是「讓模型一次寫出完美論文」，而是一條很短、也很嚴的迴路：猜、查、改。
數學問題先被寫成機器讀得懂的目標——不是「顯然成立」，而是一條有類型、有假設、有結論的形式化陳述。接著輪到 AI。它做的是搜尋，不是頒獎：根據目前還缺哪一步，提出草稿、戰術（tactic），或下一個看起來最像路的動作。有人用大語言模型直接寫證明腳本，有人在證明樹上做搜尋，有人把兩者接在一起。稱呼可以很炫，工作本質都一樣——產生候選。
候選本身沒有權威。權威在 Lean。
Lean 的小核心只做一件不討喜的事：這一步類型對不對、引用合法不合法、目標有沒有真的被消掉。過了，才算走了一步；沒過，就丟回錯誤訊息。模型再帶著「哪裡破功」去重試。成功不是語氣篤定，是迴路停在「機器核可的正式證明」上。
所以這套架構裡有兩個角色，千萬別搞混。AI 負責想像力，像一位很會編故事、偶爾還會抄近路的研究生；Lean 負責門禁，像一位不吃「顯然」、不吃「不難看出」的審查委員。研究生可以通宵改稿，委員只在手稿過關時蓋章。
這也解釋了為什麼近年大家愛把模型和 Lean 綁在一起。模型擅長在巨大的可能性裡跳，證明器擅長把跳錯的那幾下當場抓出來。少了前者，搜尋空間大到像在黑夜里找門；少了後者，你得到的可能只是一篇讀起來很像證明的散文。
AI theorem proving 不是讓機器變聰明到不會錯，是讓它被允許錯，但每一次錯都必須被檢查、被退回、被改寫。猜可以華麗，查必須刻薄。迴路能轉起來，證明才開始像證明。
--
Lean4 介紹可以看之前寫的這篇：
--
在 Lean4 安裝前, 有個 PlayGround , 可以先玩看看這個 自然數遊戲
LEAN 遊戲服務器 - Nature Number Game
--
Lean4 安裝
可以用官網這個, 先安裝 VSCode 再安裝 套件
https://lean-lang.org/install/
也可以用這個, 直接用指令方式
--
先別急著證定理：elan 管版本，lake 管開工
Lean 4 裝好之後，你真正天天碰到的通常不是那個叫 lean 的編譯器本尊，而是站在門口的兩位小管家。
一位叫 elan，管「今天用哪一版 Lean」。另一位叫 lake，管「這個專案怎麼長出來、怎麼編、怎麼跑」。前者像衣櫃管理員，後者像工地主任。衣櫃亂了，工地再整齊也會編到一半發現版本不對；工地沒人指揮，光有正確版本也只是一堆散落的 .lean 檔。
elan：別讓每個資料夾活在平行宇宙
Lean 改得快。Mathlib 更是幾乎釘死某一版。你若把「系統裡那一份 Lean」當成全世界唯一真相，過兩週就會遇見經典悲劇：A 專案要 v4.14，B 專案要 v4.32，你的終端機只認其中一個。
elan 的解法很老派，也很有效。它在你的 PATH 裡放的 lean、lake，其實是代班窗口；真正用哪一套，先看這個資料夾有沒有 lean-toolchain。有，就用上面寫的那一版，沒有就下載。專案自帶版本號，人就少做一次「我以為我在用新的」。
日常只需幾句：
Bash
elan show
elan toolchain install leanprover/lean4:stable
elan default leanprover/lean4:stableshow 是照鏡子：已安裝哪些、此刻啟動的是哪一套、是不是被眼前這個 lean-toolchain 覆寫。toolchain install 是把某一版請回家。default 是沒有專案檔時的備案。至於安裝 elan 本身，官方程式仍是那條經典的 elan-init.sh——裝完以後，請記得讓 ~/.elan/bin 出現在 PATH 裡，否則你會覺得全世界都還沒發明 lake。
一句話：elan 不幫你寫證明，它只保證你寫證明時，用的是專案同意的那台機器。
lake：Lean 界的工地主任
Lake 的全名可以記成 Lean Make。它是建置系統，也是套件管理員。設定檔叫 lakefile.toml（也可寫成 lakefile.lean），依賴、函式庫、可執行檔，都在裡面登記。產物進 .lake/，平常當它不存在就好，別手癢把編譯結果當源碼提交。
真正常用的，幾乎就是你點名的三個：new、build、exe。
lake new：先有地盤
Bash
lake new myproject # 預設模板 std：函式庫 + 可執行檔
lake new myapp exe # 只要程式
lake new mylib lib # 只要庫
lake new myproofs math # 數學向，連 Mathlib 與基本 CI 都幫你鋪好
new 會開一個新資料夾，放進 lakefile、lean-toolchain、起始 .lean。已有空資料夾、只差初始化時，改用 lake init。模板最後那個 exe、lib、math 是「專案要長成什麼樣子」，和下面要講的指令 lake exe 不是同一件事——一個是蓋房子的圖紙，一個是蓋完後開門進去跑。
若想在開張當下就釘死版本，可以讓 lake 透過 elan 指定：
Bash
lake +leanprover/lean4:v4.32.1 new myproject
加號後面是工具鏈，不是裝飾。
lake build：把字編譯成可檢查的東西
進到專案目錄：
Bash
cd myproject
lake build這一步會依 lakefile 把預設目標編起來，依賴不夠就去取，過期了就重編。可執行檔編完通常在 .lake/build/bin/。它不華麗，但誠實：紅字出現時，問題在類型、導入或設定，很少是「大概沒編到」。
第一次拉 Mathlib 的人，請先做一件會讓未來自己感謝自己的事：
Bash
lake exe cache get這不是在「執行你的程式」，而是跑 Mathlib 提供的快取工具，把別人已經編好的 .olean 搬回來。省略這步，等於堅持用自己的筆電從零砌一座數學城。
lake exe：編完，順便跑
Bash
lake exe myproject
lake exe myproject -- --helplake exe 會找到 lakefile 裡登記的可執行目標，過期就先編，再在 Lake 備好的環境裡跑起來。後面若要傳參數給程式本身，慣例是先 --，免得 lake 以為那些旗標是給它的。別名是 lake exec。
所以同一週你可能會見到兩種長得很像的句子：lake new hello exe 是「開一個只有執行檔的專案」；lake exe hello 是「把叫 hello 的執行檔編起來並執行」。前者誕生專案，後者使用專案。
一條夠用的最短路徑
大多數人的第一個下午，其實只有這幾步：
Bash
# 0. 先有 elan（之後 lean / lake 才會聽你的話）
elan show
# 1. 開工
lake new hello
cd hello
# 2. 編
lake build
# 3. 跑
lake exe hello若這是數學專案，把第一步換成 lake new hello math，進門先 lake exe cache get，再 lake build。
工具的哲學和上一篇那個「猜、查、改」其實同一款脾氣：elan 讓版本不再靠記憶，lake 讓建置不再靠咒語。你仍得自己寫那些定理；它們只負責一件更沒面子、也更重要的事——別讓開工儀式，比證明本身還難。
==
所以我一開始先 lake new my_first_lean_project
https://github.com/neojou/lean_study/tree/main/my_first_lean_project
這個 lakefile.toml 可以想成是專案設定檔,
要注意 lean_lib 是編譯成 lib/modules , 但不能直接 lake exe xxxx , 要執行需要有 lean_exe 的設定
Lean 同樣看 main 當作執行 entry, 定理驗證這些其實在靜態編譯時就完成了;
% lake build
Build completed successfully (494 jobs).
% lake exe my_first_lean_project
Hello, world!
1 + 1 = 2
1/2
3/4
5/4
看到這個就表示安裝完成了!
留言
張貼留言