Lean 4 环境搭建指南：3 步在 VSCode 里跑起交互定理证明-开发者社区

Lean 4 环境搭建指南：3 步在 VSCode 里跑起交互定理证明

【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4

Lean 4 是一门函数式编程语言，同时也是一个定理证明器——你写的每一行代码、每一条引理，都会在输入的瞬间被类型检查器盯着看，错了立刻标红。要让这套"实时验证"体验在你的电脑上跑起来，核心其实是装对两样东西：版本管理器 elan 和 VSCode 的 Lean 4 扩展。下面这份 Lean 4 环境搭建指南按"先装对工具链、再配编辑器、最后补刀坑点"的顺序展开，跟着做 15 分钟左右能出第一个Hello, world!。

🧩 先搞清一个坑：为什么别直接装编译器

Lean 4 迭代很快，不同项目往往钉在不同编译器版本上。如果你手动装一个固定版本的lean，打开别人的项目时几乎必然撞版本。elan 的存在就是为了解决这件事：它类似 Rust 的 rustup，每个项目根目录的lean-toolchain文件声明了要用的版本，elan 会按目录自动切换，终端和编辑器里拿到的是同一个正确版本。

所以安装顺序是：先装编译依赖（如果你还要从源码构建编译器），再装 elan。依赖一次装齐，GMP 数学库、libuv 异步 I/O、CMake 和 Clang 都在里面：

sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf

接着这条命令会下载并执行 elan 官方安装脚本，顺带装好一个稳定版 Lean 4：

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

装完关掉再重开一个终端，跑一下这条命令验证工具链是否就绪：

lean --version

能打印出版本号，说明 Lean 4 工具链部分已经通了。

💻 让 VSCode 成为你的交互证明工作台

编辑器装的是 Lean 4 扩展：在 VSCode 扩展市场搜 "lean4" 安装即可。它负责语法高亮、智能补全，以及右侧的 Lean Infoview——你写def或theorem时，这里会实时显示目标状态、未解决的子目标（sorry 计数）和报错，这就是 Lean 4 交互式定理证明的核心界面。

装好扩展后不用去翻设置文档：按Ctrl+Shift+P打开命令面板，输入 "Setup Guide"，选 "Docs: Show Setup Guide"，就能唤出内置的安装向导。

向导把环境搭建成了一条清单：安装依赖、装 elan、建项目，逐项打勾，卡在哪个环节点哪个环节，比看十页文档都直观。

向导走完后，建项目只需要两条命令。第一条生成脚手架（含lakefile.toml和lean-toolchain），第二条编译：

lake new my_project && cd my_project && lake build

lakefile.toml是 Lake 构建系统的入口，lake new生成的最小形态长这样，模块会自动按源码目录发现，你基本不用手改：

name = "my_project" version = "0.1.0"

想动手确认一切正常，跑这条命令用解释器直接执行文件里的main：

lake env lean my_project.lean

终端打出Hello, world!就说明从语言服务器到工具链的整条链路都通了。

🏗️ 进阶：想改编译器本身时从源码构建

如果你不是用 Lean 4，而是想给 Lean 4 本身提代码，那上面装好的只是"用户侧"环境。官方文档里的构建说明给了最短路径，克隆仓库后两条命令出一套 release 构建：

git clone https://gitcode.com/GitHub_Trending/le/lean4 cd lean4 cmake --preset release make -C build/release -j$(nproc)

几个实用细节：ccache在依赖列表里不是摆设，重新编译生成代码时它能明显提速；-j后面的数字就是并行度，核多就多给；调试编译时换--preset debug即可。构建出的stage1二进制可以通过 elan 的elan toolchain link挂成自定义工具链，让编辑器直接用你刚编译出来的版本。

🛠️ 避坑指南：三个高频报错

WSL 下提示找不到 Lean 版本

在 Windows 的 WSL 里用 Lean 4，最常见的报错是扩展提示 "Could not find Lean version by running 'lean --version'"。原因几乎都是扩展装错了位置：lean4 扩展必须装进 WSL 内部（扩展页面上的 "Install in WSL: Ubuntu"），而不是 Windows 侧，然后Ctrl+Shift+P选 "Remote-WSL: Open Folder in WSL..." 打开项目。配好后的界面长这样，右侧 Infoview 和底部终端都工作正常：

另一个隐性坑：如果 VSCode 的lean4.serverLogging.path被设成了 Windows 路径，日志就会写到 WSL 文件系统外面去。把它设成相对路径即可，日志会落在项目目录的logs文件夹里：