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 以上。各系统怎么选路线一张表说清系统推荐路线关键命令预期耗时Windows 10/11WSL2 里的 Ubuntuwsl --install偏长中间要重启一次macOS 10.15仓库自带脚本scripts/install_macos.sh较短脚本一路自动Debian/Ubuntu仓库自带脚本scripts/install_debian.sh较短脚本一路自动其他 Linux 发行版手动装 Elanelan-init.sh一行流几分钟下面三个系统殊途同归终点都是同一件事装好 Elan 和编辑器。公共底座Elan 与编辑器Elan 是「Lean 的工具链管理器」它负责下载并切换不同版本的 Lean后面所有lean、lake命令都由它托底。编辑器统一用 VS Code再装leanprover.lean4插件官网下载安装代码里哪里出错会直接标红。Windows先 WSL2再照 Linux 装微软在 Windows 上跑 mathlib4 兼容性一般标准做法是套一层 WSL2Windows 里的 Linux 子系统。打开管理员 PowerShellwsl --install看到安装提示后重启电脑 ⚠️重启完去 Microsoft Store 装一个 Ubuntu 发行版首次启动时按提示创建用户名和密码。接着把这行贴进 Ubuntu 终端装依赖sudo apt update sudo apt upgrade -y再装 git 和 curlsudo apt install -y git curl最后装 Elan一行命令选默认配置即可curl https://elan.lean-lang.org/elan-init.sh -sSf | sh装完关掉终端再重开跑lean --version输出 Lean 4 的版本号 ✅ 底座就绪。macOSHomebrew 打底脚本收尾打开终端先确认 HomebrewmacOS 的包管理器在不在/bin/bash -c $(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)没有输出错误 已就绪。然后补齐依赖brew install git curlbrew不报错 ✅ 依赖到位。最后运行仓库的 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。LinuxDebian/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 等没有现成脚本手动装 Elancurl https://elan.lean-lang.org/elan-init.sh -sSf | shVS Code 装好后补一行插件安装code --install-extension leanprover.lean4插件装完打开任意.lean文件不再提示安装扩展 ✅ 编辑器就绪。让 mathlib4 一次构建通过底座铺好下面是一条连续流水线克隆 → 缓存 → 构建 → 测试 → 跑示例。前两步可以省掉后面的漫长等待别跳。克隆仓库。把源码拉到本地git clone https://gitcode.com/GitHub_Trending/ma/mathlib4.git cd mathlib4本地出现Mathlib/、lakefile.lean ✅ 源码到手。下载预编译缓存。lake exe cache get会拉一批别人编译好的中间产物这是首次构建不熬几个小时的关键lake exe cache get下载进度条走到底 ✅ 缓存就位。构建 mathlib4。编译整个数学库lake build✅ 结束时无报错、无 error 输出 构建通过。首次没拿到缓存的话这一步会非常慢 ⚠️。跑测试。验证环境确实配对了lake test测试全部通过 ✅ 环境合格。跑一个示例程序收尾。以 LongestPole 为例cd LongestPole lake build lake exe Main看到程序输出而不是编译错误 ✅ 全链路打通。避坑速查卡住了先对下表大多是一行命令的事现象可能原因一行修复命令lake exe cache get拉不到有效缓存缓存状态过期lake exe cache get!构建产物坏掉、反复报错本地残留旧构建文件先lake clean再lake exe cache getlean: command not foundElan 没进 PATH重开终端仍不行就重装 Elan想装/切别的 Lean 版本工具链版本不符elan toolchain install 4.0.0再elan default 4.0.0不确定现在装了哪些版本需要盘点elan toolchain listVS 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创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
