Lean 4 开发环境从零搭起来：新手四步走完到第一个可运行项目
【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4
Lean 4 是一门兼具函数式编程与定理证明能力的语言。本文面向零基础新手：跟着读完，你会装好工具链、建出第一个项目并在 VSCode 中获得实时的证明反馈。
先记住目标：环境搭好的四个判断信号
在动手之前，先记住下面四组信号，全部出现就说明环境就绪：
- 终端里运行
lean --version能看到版本号，而不是提示命令不存在。 lake build执行完毕且没有报错，项目目录中出现.lake目录。- VSCode 打开项目后，右侧 Infoview 面板出现，并显示光标所在行号。
- 运行程序后终端打印出
Hello, world!。
下文就是围绕这四条逐一落地的过程。
动手之前：先分清"使用 Lean"和"从源码编译 Lean"
绝大多数新手属于第一类——写 Lean 代码。这种情况只需要安装 elan 工具链管理器，它会自动下载匹配的编译器版本，不需要任何额外依赖。
只有当你想修改或重新编译 Lean 4 编译器本身时，才需要 C++ 编译器、CMake、GMP、LibUV、OpenSSL 等构建依赖。Ubuntu 上一条命令即可备齐：
sudo apt-get install git libgmp-dev libuv1-dev libssl-dev cmake ccache clang pkgconf安装过程无报错、命令正常返回提示符，说明依赖到位。源码仓库地址是 https://gitcode.com/GitHub_Trending/le/lean4 ，克隆后用 CMake 配置、make 并行编译，仓库文档里给出了完整的构建参数与排错说明。
🚀 最短路径：一条命令装 elan，三条命令建项目
elan 是 Lean 4 版本管理的统一入口：不同项目可以依赖不同的编译器版本，elan 负责自动匹配和下载。
先执行官方安装脚本：
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh脚本下载并执行到结束、全程没有错误输出，即安装成功。接着创建第一个项目：
lake new hello_lean cd hello_lean lake build终端出现Build completed successfully.，并且项目目录下多出一个.lake文件夹，说明项目已建立并完成首次构建。
验证闭环：三个动作确认环境真的能跑
装完不等于能用，按顺序做三个动作才算闭环。
动作一，确认编译器版本可读取：
lean --version输出一行形如Lean (version 4.x, ..., Release)的文字，说明 elan 与编译器已正确联动。
动作二，把程序跑起来：
lake exe hello_lean终端打印Hello, world!，编译到运行的链路就通了。
动作三，故意制造一个错误：在Main.lean任意一行加入1 + "a" = 5并保存。如果 VSCode 在该行标出红色波浪线、Infoview 同步显示类型错误信息，说明实时类型检查已生效。验证完删掉这一行即可。
最快接入 VSCode 的方法：让安装向导替你装
在扩展市场搜索 "Lean 4" 并安装扩展，即可获得语法高亮、自动补全与错误标注，这是接入成本最低的方式。
首次打开项目时，扩展可能自动弹出安装向导；如果没有，从扩展菜单的 Docs 项选择 "Show Setup Guide" 手动打开。向导的第一步就是安装 elan：点击安装按钮后，脚本会自动下载并执行。每一步完成后条目会打上对勾，最后一步 "Questions and Troubleshooting" 则汇总了常见问题的处理文档。
接入成功的标志：编辑器右上角出现 Infoview 面板，形如Foo.lean:2:28的位置信息和 "No info found." 占位文字，说明 Lean 语言服务器已经启动并跟踪当前文件。
WSL 或远程开发怎么连
如果代码放在 WSL 或远程机器上，再装一个 VSCode 的 "Remote Development" 扩展包，以 WSL 模式打开项目，文件读写与终端都会运行在 Linux 内部。
看到左侧文件树显示 WSL 中的项目、终端出现(base) user@host:~$提示符、右侧 Infoview 能正常显示当前行反馈，连接即正常。
日常使用：边写代码边看证明反馈
接入之后，日常开发主要靠三个高频操作。
看证明状态：光标停在证明步骤末尾，Infoview 会显示该位置当前的目标，这是 Lean 4 交互式证明的核心用法。
查常量信息：把光标放在某个名称上，使用 "Show Term" 命令即可查看完整类型与定义。
插入交互组件：在代码里写一行#widget命令，扩展会在编辑器内渲染出可交互内容，例如魔方演示：
#widget rubiks {seq := ["U", "L", "R", "L+", "R"]}#widget行出现后 Infoview 显示加载条，渲染完成即可直接在编辑器里转动魔方，这就是 Lean 4 的 widget 能力。
🔍 版本冲突和常见卡点怎么处理
项目与系统的 Lean 版本不一致：这不是故障，而是设计如此。elan 会读取项目内的lean-toolchain文件，自动使用（必要时下载）项目指定的版本。若需手动调整全局默认版本：
elan toolchain install stable elan default stable随后运行lean --version，输出的版本号变为新版即切换成功。
提示lean命令不存在：elan 把路径写进了新终端的环境变量。关闭并重开终端，或执行source ~/.bashrc后重新验证。
从源码编译时定位不到错误：给 make 追加VERBOSE=1参数，它会逐条打印实际执行的命令，便于锁定失败的那一步。
延伸资源：文档、示例与测试用例
环境跑通后，可以用仓库里三个目录继续练习：
- doc/：官方文档，覆盖安装、开发指南与各语言特性章节。
- doc/examples/：可直接编译运行的示例程序，适合照着写自己的证明。
- tests/：项目的测试用例集合，是熟悉报错信息与高级语法的好素材。
下一步建议：在 hello_lean 项目里用by decide证明2 + 2 = 4，再换成一个需要omega战术的命题。卡住时先翻安装向导里的 "Questions and Troubleshooting"，绝大多数卡点都写在里面。
【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4
创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
