1.3 環境建置#

本節目標#

• 安裝 Lean 版本管理器 elan 與 Lean 工具鏈
• 建立第一個使用 Mathlib 的 Lean 專案
• 設定 VS Code 與 lean4 擴充功能
• 學會看 Infoview（goal state）介面
• 認識常見安裝問題與解法

安裝 elan#

elan 是 Lean 的版本管理器（類似 Rust 的 rustup）。它會依專案需求自動下載對應版本的 Lean 編譯器。

macOS 與 Linux#

打開終端機，執行：

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

安裝過程中若詢問是否修改 PATH，直接按 Enter 採用預設即可。完成後重開終端機（或執行 source ~/.profile），驗證：

elan --version
lake --version
lean --version

注意：macOS 使用者若沒有 Apple 開發者工具，系統會自動提示安裝 Command Line Tools，照著裝即可。

Windows#

官方建議使用 WSL2（Windows Subsystem for Linux），在 WSL 中照 macOS/Linux 的方法安裝。若堅持原生 Windows，下載 elan-init.exe 執行：

# PowerShell 中
.\elan-init.exe

本書建議：Windows 使用者裝 WSL2，之後的所有指令都在 WSL 的 bash 裡執行，可以少踩很多坑。

建立第一個專案#

Lean 用 lake 管理專案與依賴（類似 cargo 之於 Rust、npm 之於 Node.js）。

lake new myproj
cd myproj

生成的專案結構：

myproj/
├── lean-toolchain      # 指定 Lean 版本
├── lakefile.toml       # 專案設定與依賴
├── Myproj.lean         # 函式庫根檔案
└── Myproj/
    └── Basic.lean      # 你的程式碼放這裡

lean-toolchain：版本釘選#

lean-toolchain 檔案內容只有一行，例如：

leanprover/lean4:v4.15.0

它告訴 elan：「這個專案要用 v4.15.0 的 Lean」。當你 cd 進專案目錄，elan 會自動切換到正確版本——這就是為什麼不同專案可以用不同版本的 Lean 而互不干擾。

重要：Mathlib 版本必須與 Lean 版本完全對應。最省事的做法是：以 Mathlib 官方範本建立專案，讓兩者自動對齊（見下節）。

lakefile 依賴 Mathlib#

修改 lakefile.toml（Lean 4 新式設定檔），加入 Mathlib 依賴：

name = "myproj"
version = "0.1.0"
defaultTargets = ["Myproj"]

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.15.0"

（若你的專案生成的是 lakefile.lean，語法是：

import Lake
open Lake DSL

package «myproj» where

@[require_mathlib]
require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @"v4.15.0"

@[default_target]
lean_lib «Myproj» where

）

然後下載 Mathlib 原始碼與快取：

curl -L https://raw.githubusercontent.com/leanprover-community/mathlib4/master/lean-toolchain -o lean-toolchain
lake exe cache get
lake build

lake exe cache get 是關鍵：Mathlib 編譯完整版要好幾個小時，快取機制讓你直接下載社群已編譯好的二進位檔，幾分鐘就能用。每次 Mathlib 版本更新後都要重新執行一次。

最推薦的做法：直接用官方範本，省去手動對齊版本的麻煩：

curl https://raw.githubusercontent.com/leanprover-community/mathlib4/master/scripts/elan-init.sh -sSf | sh -s -- myproj
cd myproj && lake exe cache get

VS Code 與 lean4 擴充#

1. 安裝 Visual Studio Code。
2. 在擴充市集搜尋 lean4（發布者是 leanprover-community），安裝。
3. 用 VS Code 打開你的專案資料夾（code myproj），lean4 擴充會自動偵測 lean-toolchain。
4. 打開任何 .lean 檔案，右下角出現「Lean: ...」狀態列，表示語言伺服器啟動中；變成綠色/勾勾即就緒。

編輯 .lean 檔時，VS Code 會即時呼叫 Lean 檢查每一行，錯誤會以紅色底線呈現，跟寫 TypeScript/Python 的體驗類似。

Infoview（目標狀態）介面導覽#

這是 Lean 學習曲線中最重要的一塊。把游標放在證明中的某一行，VS Code 右側會出現 Infoview 面板，即時顯示該位置的「證明狀態」。

假設檔案內容是：

example (a b : ℕ) (h : a ≤ b) : a + 0 ≤ b := by
  rw [Nat.add_zero]
  exact h

把游標放在 rw [Nat.add_zero] 那一行，Infoview 大致長這樣（文字示意）：

Goals (1)
a b : ℕ
h : a ≤ b
⊢ a + 0 ≤ b

解讀：

• 上半部是本地脈絡（context）：目前手上有的變數與假設。這裡有兩個自然數 a b，和一個假設 h : a ≤ b。
• 符號 ⊢（turnstile，讀作「turnstile」）右邊是目前要證的目標，這裡是 a + 0 ≤ b。
• 當你把游標往下移一行，目標變成 a ≤ b（因為 rw 已把 a + 0 改寫為 a）。
• 當你完成證明（游標在最後一行之後），Infoview 顯示 "No goals"——證明完畢！

這就是與 Lean「對話」的方式：每寫一行戰術，看一眼 Infoview，確認目標朝正確方向變化。它就像除錯時的變數監看面板，只是監看的對象是「邏輯狀態」而非「記憶體狀態」。

常用操作：

• 游標移到任何一行：Infoview 顯示該處狀態。
• Ctrl+Shift+Enter（macOS：Cmd+Shift+Enter）：切換 Infoview 顯示/隱藏。
• 把游標放在某個函式或引理名稱上：Infoview 顯示它的完整型別與文件。

常見安裝問題#

一個心智模型：Lean 專案 = 「Lean 版本 + Mathlib 版本 + 你的程式碼」三者的精確鎖定。三者任何一個對不上，都會報錯。用範本建立專案可以避免九成的版本地獄。

小結與練習#

本節重點#

1. elan 管理 Lean 版本，lake 管理專案與依賴。
2. Mathlib 依賴要與 lean-toolchain 版本精確對應，用官方範本最省事。
3. lake exe cache get 下載預編譯快取，是使用 Mathlib 的必經步驟。
4. Infoview 顯示「脈絡 + 目標」，是與 Lean 對話的核心介面。

練習#

1. 完整走一遍安裝流程，成功執行 lake build 並讓專案編譯通過。
2. 在 Myproj/Basic.lean 裡輸入 #check 1 + 1，觀察 Infoview 顯示什麼。
3. 把游標分別放在證明的第一行與最後一行，比較 Infoview 內容的差異。
4. （進階）故意把 lean-toolchain 改成另一個版本號，執行 lake build，觀察錯誤訊息，然後改回來。你現在知道版本地獄長什麼樣了。

下一節，我們寫出你的第一個 Lean 證明。