Lean 4是一個功能強大的交互式定理證明器和程序驗證工具，如果能夠聯網，可以很容易就按照官方的安裝指南來進行安裝，但是在國內如果要給一臺不能連網的設備進行環境安裝，這方面的指南卻比較少。 本文將詳細介紹如何在Linux x86-64系統的離線環境中完整安裝Lean 4開發環境，包括必要工具和VS Code插件的配置。同樣的步驟和原理也適合在其他平臺（如windows）上嘗試。

一、準備工作

1. 在線環境下載必要文件

在聯網的計算機上，從以下地址下載所需文件：

1. VS Code Lean 4插件
   從VS Code Marketplace下載.vsix文件：

   leanprover.lean4-0.0.206.vsix
   

2. elan工具鏈管理器
   從GitHub Releases或上海交通大學鏡像源下載對應平臺的包：

   https://s3.jcloud.sjtu.edu.cn/899a892efef34b1b944a19981040f55b-oss01/elan/mirror_clone_list.html
   

   選擇文件：

   elan-x86_64-unknown-linux-gnu.tar.gz
   

3. Lean 4二進制包
   同樣從上海交通大學鏡像源下載指定版本的Lean 4：

   lean-4.20.0-linux.tar.zst
   

2. 傳輸文件至離線環境

將上述下載的文件復制到目標離線Linux系統（建議創建專用目錄如~/lean4-offline-install/）。

二、安裝elan工具鏈管理器

1. 解壓并安裝elan

# 進入存放下載文件的目錄
cd ~/lean4-offline-install/# 解壓elan安裝包
tar xvf elan-x86_64-unknown-linux-gnu.tar.gz# 賦予執行權限并安裝
chmod +x elan-init
./elan-init -y --default-toolchain none

2. 配置環境變量

編輯Shell配置文件（如.bashrc或.zshrc）：

echo 'export PATH="$HOME/.elan/bin:$PATH"' >> ~/.bashrc
# 或對于Zsh用戶
echo 'export PATH="$HOME/.elan/bin:$PATH"' >> ~/.zshrc# 使配置立即生效
source ~/.bashrc  # 或 source ~/.zshrc

3. 驗證elan安裝

elan -V  # 查看版本
elan show  # 顯示工具鏈信息

三、安裝Lean 4二進制包

1. 解壓Lean 4二進制文件

# 解壓Lean 4包（使用tar的zst格式支持）
tar xvf lean-4.20.0-linux.tar.zst# 創建安裝目錄（可選）
mkdir -p ~/lean4/
mv lean-4.20.0-linux ~/lean4/

2. 注冊工具鏈到elan

# 將解壓的Lean 4版本注冊到elan
elan toolchain link stable ~/lean4/lean-4.20.0-linux# 驗證工具鏈
elan show

四、安裝VS Code Lean 4插件

1. 使用VS Code界面安裝插件

1. 打開VS Code
2. 點擊左側邊欄的擴展圖標（或按Ctrl+Shift+X）
3. 點擊右上角的**…，選擇從VSIX安裝**
4. 瀏覽并選擇之前下載的leanprover.lean4-0.0.206.vsix文件
5. 等待安裝完成后，點擊重新加載

五、使用VS Code界面創建Lean 4工程

1. 創建新項目

1. 打開VS Code
2. 點擊文件 → 打開文件夾，選擇或創建一個空文件夾（例如lean4-project）
3. 在終端中執行（通過VS Code的集成終端：`Ctrl+``）：

   lake init lean4-project  # 初始化Lean 4項目
   

2. 配置項目

1. 打開項目根目錄下的lakefile.lean文件
2. 確保配置包含以下內容：

   import Lakepackage lean4-project where-- 項目配置-- 如需添加依賴，可在此處修改-- Lean 4標準庫依賴
   require lean from git "https://github.com/leanprover/lean4" @ "v4.20.0"
   

3. 創建第一個文件

1. 在項目根目錄下創建Main.lean文件
2. 輸入以下內容：

   def add (a b : Nat) : Nat := a + b#eval add 3 5  -- 應輸出8
   

六、驗證安裝

1. 檢查VS Code集成

1. 在VS Code中打開Main.lean文件
2. 等待Lean 4服務器啟動（底部狀態欄顯示"Lean 4: Ready"）
3. 將光標放在add函數上，應顯示類型信息
4. 運行#eval命令，查看輸出結果

七、故障排除

1. 環境變量問題

如果elan命令無法找到，檢查：

• ~/.elan/bin是否已添加到PATH
• Shell配置文件是否正確加載

2. 工具鏈未識別

如果VS Code無法找到Lean 4：

• 檢查elan show輸出是否顯示stable工具鏈
• 手動設置lean4.path為~/lean4/lean-4.20.0-linux/bin/lean

3. 插件兼容性問題

確保下載的.vsix版本與Lean 4版本兼容，可嘗試更新到最新插件版本。

總結

通過上述步驟，你已在離線Linux環境中成功安裝了Lean 4開發環境，包括elan工具鏈管理器、Lean 4二進制包和VS Code集成插件。這種安裝方式不依賴網絡連接，適合在受限環境中進行形式化驗證和定理證明工作。