Lean 4 形式化验证实战指南配好环境写出第一条交互式证明看懂定理证明器的目录结构【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4Lean 4 是一门编程语言兼定理证明器也是目前做形式化验证最常用的工具之一。在同一个文件里你既可以写函数也可以写关于这个函数的证明——这个排序确实有序这个查找函数不会越界——而证明的每一行都会被内核机械地核对通过即数学意义上成立而不是测试覆盖了几种场景。本文带你用 VS Code 配好 Lean 4 开发环境写出第一条交互式证明并带你把源码仓库的目录结构看明白。从一个具体任务说起证明回文列表的逆序仍是回文假设你要实现一个处理回文列表的工具函数。在普通语言里回文只能写在注释或断言里在 Lean 4 里它可以直接写进类型系统。官方示例 doc/examples/palindromes.lean 的做法是先用归纳命题定义什么叫回文再对定义做归纳来推导性质theorem palindrome_reverse (h : Palindrome as) : Palindrome as.reverse : by induction h这条定理说的是只要as是回文它的逆序as.reverse也一定是回文。证明过程写在编辑器里内核逐行检查每一步推理是否合法漏掉一种情况光标处立刻报错。更进一步依赖类型能让前提直接进入函数签名——同一个示例里定义的List.last取列表最后一个元素要求调用方先证明as ≠ []也就是说对空列表取最后一个元素这类边界错误在写代码的阶段就被拦下了根本轮不到运行时。这个文件只有 120 行左右注释完整是理解 Lean 4 工作方式的好起点。用 VS Code 装好 Lean 4安装向导与 Elan 版本管理器对绝大多数使用者不需要从源码构建 Lean 4走 VS Code 的安装向导即可在 VS Code 里安装 Lean 4 扩展打开工作区后欢迎页会出现 Lean 4 Setup 设置页列出四步打开设置向导、书籍与文档、安装依赖、安装版本管理器 Elan。按页面提示点击安装 Elan。Elan 是 Lean 生态的版本管理器负责为每个项目自动下载匹配的 Lean 工具链——仓库根目录的lean-toolchain文件声明了该仓库使用的工具链版本Elan 读取它之后保证你和同事、CI 跑的是同一个版本。之后打开任意 Lean 项目工具链会自动就位可以直接编写和检查.lean文件。日常使用中还会用到命令面板。CtrlShiftPmacOS 为CmdShiftP唤出后Docs 子菜单下有 Show Setup Guide重新打开设置向导、Show Manual、Unicode 输入缩写说明等入口排查环境问题时比较顺手。只有想修改 Lean 4 本身比如给编译器加功能、修内核 bug的开发者才需要从源码构建git clone https://gitcode.com/GitHub_Trending/le/lean4各平台Ubuntu、macOS、Windows/MSYS2、WSL的依赖清单和构建命令在 doc/make/index.mdLinux/macOS/WSL 用户也可以直接用nix develop一条命令进入构建环境。构建产物的自举机制另见 doc/dev/bootstrap.md。第一条交互式证明怎么写InfoView、即时反馈与 widgets装好环境后打开一个.lean文件典型的开发界面分四个区域左侧项目文件树、中间代码编辑区、右侧 Lean InfoView、底部终端。InfoView 是交互式证明的核心——把光标停在某一行它就显示这一行的上下文当前的证明目标、可用的假设、以及#print等命令的输出出错的行会直接在代码里标出不需要等到编译结束。几个日常最常用的即时命令都放在文件任意位置即可执行#check查看一个表达式的类型#eval直接运行表达式并打印结果例如#eval List.range 5#reduce观察定义如何被化简。Lean 4 还有一个容易被忽略的能力widgets。在 Lean 文件里写一行#widget命令InfoView 会加载对应的 JavaScript 组件并渲染成可交互的图形。官方示例 doc/examples/widgets.lean 就实现了下面这个魔方演示——输入一个转动序列右侧同步渲染出 3D 魔方状态用来给抽象概念做可视化非常直观#widget rubiks {seq: [U, L, R, L, R]}看懂源码仓库各目录干什么用Lean 4 的仓库本身就是一个大型教学样本。第一次浏览建议按下表定位再配合 doc/ 下的开发文档深入目录作用src/kernel/C 实现的内核表达式表示、类型检查type_checker.cpp、环境管理environment.cpp。所有证明最终都在这层被校验是最后一道关src/Init/预置标准库语言内建类型与基础数据结构Prelude.lean、Data/、Control/src/Std/扩展标准库Tactic/证明策略、Data/数据算法、Time/计时、WP/最弱前置条件等src/Lean/语言工具的实现Elab/词法语法到类型的加工、Meta/元编程、Compiler/生成机器码、Linter/代码检查、Server/IDE 协议src/lake/Lake 构建与包管理工具doc/examples/官方示例二叉树、回文、widgets 等全部被 CI 检查保证每版可用tests/测试套件elab/、elab_fail/期望报错的用例、compile/、lake/等共数千个用例stage0/预编译快照供自举构建使用普通使用者无需关心想给 Lean 4 提改进先读 CONTRIBUTING.md想了解各版本行为变化查 RELEASES.md。对比Lean 4 形式化验证能做与不能做的事把 Lean 4 和日常工具放在一起看边界会更清楚维度Lean 4 形式化验证常规静态类型检查单元测试回答的问题某性质对所有输入成立数学证明某类类型错误不存在手工挑选的示例得到预期输出覆盖范围证明写到哪里覆盖到哪里类型系统能表达的规则子集取决于测试用例写了多少反馈时机证明过程中即时显示缺口编译时运行测试时书写成本最高需学习策略与命题表述最低中等附带产物经验证的定理 可直接编译运行的代码无无需要说清楚的不能形式化验证不会替你自动验证一切。性质必须先被准确地表述成命题而把正确性写成机器可检查的形式本身往往比实现功能更费脑力对业务逻辑复杂、变更频繁的系统前期投入是否划算需要自己评估。它最适合的形态是功能相对独立、正确性可以明确表述、且错误代价高的模块。何时引入 Lean 4下一步读什么比较合适的切入点验证某个关键算法的性质比如这个查找函数在任意合法输入下返回正确下标、给教学材料配可运行的证明、或者维护一个依赖类型系统的库。不合适的切入点通用业务系统的日常开发学习曲线会拖慢交付。按这个顺序往下走比较顺通读 doc/examples/ 里的 bintree.lean用二叉树实现有序映射并证明其性质和 palindromes.lean把定义命题—归纳证明—化简这套流程跑两遍浏览 doc/std/ 中的命名与风格约定naming.md、style.md写自己的库时保持一致想动手改工具链时从 doc/dev/ 的开发指南入手重点看src/Lean/Elab/和src/Lean/Meta/报错信息的产生路径在那里遇到怪行为去 tests/ 里搜相似用例尤其是elab_fail/——里面是大量故意写错并断言报什么错的样本能帮你理解编译器各层的分工。Lean 4 的仓库结构本身就说明了它的定位一半是语言与工具src/Lean/、src/lake/一半是被这套工具严格检验过的数学内容src/Init/、src/Std/、doc/examples/。把这两面都看一遍比看任何宣传材料都更能建立对形式化验证的真实预期。【免费下载链接】lean4Lean 4 programming language and theorem prover项目地址: https://gitcode.com/GitHub_Trending/le/lean4创作声明：本文部分内容由AI辅助生成（AIGC），仅供参考
