Lean 4 + mathlib4 环境搭建完整教程：三步走，一次构建通过

【免费下载链接】mathlib4The math library of Lean 4项目地址: https://gitcode.com/GitHub_Trending/ma/mathlib4

这是一份 Lean 4 环境搭建的完整教程，教你装好工具链、让 mathlib4 的lake build一次跑通。搭好之后，你可以在 VS Code 里直接做数学定理的形式化证明，写代码、跑构建、调测试，甚至参与 mathlib4 这座数学库本身的维护。

动手前的快速自检

先花 10 秒确认三件事：网络稳定（后面要拉源码和缓存）、至少 10GB 空闲磁盘、系统版本达标——Windows 10/11 64 位、macOS 10.15 以上、Linux 内核 5.4 以上。

各系统怎么选路线，一张表说清：

下面三个系统殊途同归，终点都是同一件事：装好 Elan 和编辑器。

公共底座：Elan 与编辑器

Elan 是「Lean 的工具链管理器」，它负责下载并切换不同版本的 Lean，后面所有lean、lake命令都由它托底。编辑器统一用 VS Code，再装leanprover.lean4插件（官网下载安装），代码里哪里出错会直接标红。

Windows：先 WSL2，再照 Linux 装

微软在 Windows 上跑 mathlib4 兼容性一般，标准做法是套一层 WSL2（Windows 里的 Linux 子系统）。打开管理员 PowerShell：

wsl --install

看到安装提示后重启电脑 ⚠️，重启完去 Microsoft Store 装一个 Ubuntu 发行版，首次启动时按提示创建用户名和密码。

接着把这行贴进 Ubuntu 终端，装依赖：

sudo apt update && sudo apt upgrade -y

再装 git 和 curl：

sudo apt install -y git curl

最后装 Elan（一行命令，选默认配置即可）：

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

装完关掉终端再重开，跑lean --version，输出 Lean 4 的版本号 = ✅ 底座就绪。

macOS：Homebrew 打底，脚本收尾

打开终端，先确认 Homebrew（macOS 的包管理器）在不在：

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

没有输出错误 = 已就绪。然后补齐依赖：

brew install git curl

brew不报错 = ✅ 依赖到位。最后运行仓库的 macOS 安装脚本，它会代劳 Elan 和编辑器插件：

curl -fsSL https://gitcode.com/GitHub_Trending/ma/mathlib4/raw/branch/master/scripts/install_macos.sh | bash

脚本跑完重开终端，lean --version出版本号 = ✅ 底座就绪。脚本本体见 scripts/install_macos.sh。

Linux：Debian/Ubuntu 走脚本，其他发行版手动

Debian/Ubuntu 用户先装依赖：

sudo apt update && sudo apt install -y git curl

再跑官方安装脚本，同样自动装 Elan 和插件：

curl -fsSL https://gitcode.com/GitHub_Trending/ma/mathlib4/raw/branch/master/scripts/install_debian.sh | bash

脚本无报错、lean --version有输出 = ✅ 底座就绪。脚本见 scripts/install_debian.sh。

其他发行版（Arch、Fedora 等）没有现成脚本，手动装 Elan：

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

VS Code 装好后补一行插件安装：

code --install-extension leanprover.lean4

插件装完，打开任意.lean文件不再提示安装扩展 = ✅ 编辑器就绪。

让 mathlib4 一次构建通过

底座铺好，下面是一条连续流水线：克隆 → 缓存 → 构建 → 测试 → 跑示例。前两步可以省掉后面的漫长等待，别跳。

1. 克隆仓库。把源码拉到本地：

git clone https://gitcode.com/GitHub_Trending/ma/mathlib4.git cd mathlib4

本地出现Mathlib/、lakefile.lean= ✅ 源码到手。

2. 下载预编译缓存。lake exe cache get会拉一批别人编译好的中间产物，这是首次构建不熬几个小时的关键：

lake exe cache get

下载进度条走到底 = ✅ 缓存就位。

3. 构建 mathlib4。编译整个数学库：

lake build

✅ 结束时无报错、无 error 输出 = 构建通过。首次没拿到缓存的话这一步会非常慢 ⚠️。

4. 跑测试。验证环境确实配对了：

lake test

测试全部通过 = ✅ 环境合格。

5. 跑一个示例程序收尾。以 LongestPole 为例：

cd LongestPole lake build lake exe Main

看到程序输出而不是编译错误 = ✅ 全链路打通。

避坑速查

卡住了先对下表，大多是一行命令的事：

VS Code 插件失灵时的顺序：重装插件 → 确认 VS Code 是最新版 → 在仓库根目录跑lean --version确认可执行文件找得到。

环境就绪之后的下一步

• 官方教程项目，从零写第一个证明：https://leanprover-community.github.io/install/project.html
• 仓库内置文档与概览：docs/
• 经典例题，IMO 试题、Wiedijk 百定理都在里面：Archive/Examples/
• 测试用例，看各种场景怎么用库：MathlibTest/
• 项目总览与贡献指引：README.md

搭建过程中遇到本文没覆盖的问题，先翻 README.md 里的指引；社区渠道对新手非常友好，直接提问即可，各级水平的问题都欢迎。

【免费下载链接】mathlib4The math library of Lean 4项目地址: https://gitcode.com/GitHub_Trending/ma/mathlib4