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集成插件。这种安装方式不依赖网络连接，适合在受限环境中进行形式化验证和定理证明工作。