Lean 4 完整上手指南5 步跑通带机器可验证证明的编程语言【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4Lean 4 是一个定理证明器和编程语言的结合体你用同一套语言写函数、定义类型也能把这个函数满足什么性质写成定理交给内核逐条检查——证明通过才叫通过不存在大概没问题。这篇 Lean 4 安装与入门指南面向没接触过它的开发者带你从装环境到读懂源码再到走读一个真实的认证算法例子。从证明函数是对的开始假设你实现了一个二叉搜索树插入、查找都写好了测试也全绿。但测试只能覆盖你测到的输入而插入后 BST 不变量仍成立这类性质靠测试无法穷尽。Lean 4 的做法是把不变量写成命题再用归纳法给出证明。仓库 doc/examples/bintree.lean 里就是这么干的先证明插入操作保持 BST 性质再用子类型{ t : Tree β // BST t }把合法树封装成新类型此后调用者拿到的树在类型层面就保证合法。性质不成立时证明根本编译不过——这就是 Lean 4 形式化验证与单元测试的本质区别。Lean 4 安装与环境配置5 步跑起来安装 elan这是 Lean 工具链的版本管理器一条安装脚本即可负责下载和管理特定版本的 Lean 工具链安装 VS Code Lean 扩展扩展提供补全、错误诊断和证明状态反馈创建工具链文件在项目根目录建一个lean-toolchain文件写入门槛版本号elan 会自动拉取对应工具链打开安装向导核对环境VS Code 里执行 Docs: Show Setup Guide可对照检查 elan、扩展、依赖是否就绪写一个最小例子验证新建一个.lean文件用#eval打印一个表达式能出结果即环境可用如果后面要改 Lean 本身而不是用它写代码才需要从源码构建按 doc/make/index.md 的要求装好 CMake、GMP、LibUV、OpenSSL然后cmake --preset release加make即可构建产物在stage1子目录。三个值得看的能力1. 证明即代码证明可执行Lean 4 里定理和函数一样参与类型检查。doc/examples/palindromes.lean用归纳谓词定义回文列表证明回文的逆序仍是回文只需对归纳假设做三次分支展开。更妙的是#eval [1, 2, 1].isPalindrome这种代码可以直接执行——证明和程序共存于同一个文件、同一套类型系统。2. 可组合的元编程系统Lean 的语法和证明策略tactic本身可以用 Lean 写。bintree.lean里有一个局部宏have_eq它用几行宏定义封装了用线性算术证相等、再代入目标的固定套路之后证明里直接写have_eq key k复用。这意味着团队可以把重复的证明步骤沉淀成自定义命令。3. 程序与证明互通的编译Lean 4 能把通过验证的代码编译成可执行产物并且可以用[csimp]属性让编译器在生成代码时用被证明等价的更优实现替换原实现——bintree.lean末尾就展示了先证明toList与线性时间的toListTR相等再声明编译时替换正确性由定理保证性能由替换保证。此外它还能通过 UserWidget 生成网页交互组件例如 doc/images/widgets_rubiks.png 所示的 3D 魔方就是 Lean 代码直接编译出来的。Lean 4 源码目录怎么读先读哪里这个仓库同时是语言实现和标准库第一次进源码时按下面的顺序看能少走很多弯路src/kernel/先于一切这是 C 写成的内核类型检查和定义相等判断的最终裁决者。读懂expr.h、type_checker.h这两个头文件你就理解了一个证明为什么合法的底线src/Lean/Meta/是核心中的核心约 480 个文件简化器simp、求值、元数据操作都在这里。想搞懂Lean 怎么自动化证明从Lean.Meta.Simp开始src/Init/是预编译进每个项目的基石基础类型Nat、List、Array和最常用的 tactic 都在这改动它等价于改语言本身所以它被单独放最上层src/lake/是包管理器 LakeLean 生态的构建工具用 Lean 自己实现仓库根目录的lakefile.toml就是它的配置tests/目录值得留意elab/词法解析、elab_fail/应失败的案例、compile/编译产物分门别类看测试比看实现更容易理解边界行为。一个代表性用例走读认证类型检查器doc/examples/tc.lean是理解 Lean 4 工作方式的绝佳样本它实现了给表达式推类型且这个功能本身被证明正确。链路分四步输入用归纳类型Expr定义一门只含数字、布尔和plus/and的小语言再定义归纳谓词HasType作为类型规则处理Expr.typeCheck e对表达式做模式匹配返回推断出的类型 类型正确的证明或者返回unknown。注意返回值类型是{{ ty | HasType e ty }}——类型层面就绑定了返回的类型必须真的是 e 的类型输出证明部分两个关键定理——typeCheck_correct保证如果返回 found类型一定对正确性typeCheck_complete保证如果返回 unknown该表达式确实无类型完全性。前者靠对HasType的分支穷举后者靠对表达式的归纳收尾最后把是否有类型变成一个可判定的Decidable实例调用方拿到的是可计算的结果整个流程里程序逻辑和逻辑保证是同一个文件的两个部分内核保证二者不能互相打脸。什么情况值得用它Lean 4 适合的场景正确性需要被证明而不只是被测试的系统——密码学原语、形式化语言/编译器如phoas.lean展示的高阶抽象语法嵌入、数学库开发以及你想学习用依赖类型把不变量写进类型这种编程范式。不必考虑它的场景快速原型、常规业务开发——它的编译速度、学习曲线和生态体量都决定了它不是拿来写 CRUD 的如果你的需求只是静态类型 空指针安全Rust 或 Swift 的投入产出比更高。延伸入口仓库自带一套 CI 校验过的示例在 doc/examples/从回文列表到解释器、类型检查器都有是比教程更贴近实战的起点想动手改 Lean 本身先看 doc/dev/index.md 的开发指南构建相关细节在 doc/make/index.md。【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考