Lean 4｜交互式定理证明器与函数式编程语言

工具说明

Lean 4 是一个交互式定理证明器，同时也是一门函数式编程语言。它让使用者用代码写出数学定义、定理与证明，并由系统逐条检查证明是否严密，从而把数学论证转化为可机器验证的形式。资料显示，它是 AI 形式化数学研究和自动定理证明的核心基础设施，DeepMind 的 AlphaProof 与 DeepSeek-Prover 均基于此。

适用人群

• 从事形式化数学、证明助手研究的科研人员与研究生。
• 研究 AI 自动定理证明、形式化验证的工程师。
• 想学习依赖类型与函数式编程的开发者。

已知能力

• 交互式编写与检查数学证明，错误会被明确报出。
• 作为通用函数式编程语言编写程序，并可对程序性质做形式化证明。
• 拥有配套的包管理与构建工具链、数学库生态，具体组件以官方文档为准。

使用步骤（概要）

1. 按官方文档安装工具链，管理 Lean 版本与依赖。
2. 创建工程，编写定义与定理陈述。
3. 在编辑器中逐步填充证明，借助交互反馈修正。
4. 在工程中引入所需数学库，运行构建命令检查全部证明。

费用、许可与国内使用

• 软件自身许可需查阅官方仓库与发行说明，本站未核验。
• 免费使用，安装与学习成本较高，需具备一定数学与编程基础。
• 国内下载工具链与依赖包的速度、镜像可用性待核验。
• 本站未做实测，不对性能与成效作保证。

来源与使用边界

原始入口：https://github.com/leanprover/lean4

整理来源：https://github.com/ikaijua/Awesome-AITools

依据来源资料经AI翻译整理，未由本站实测。原始资料许可：CC-BY-4.0；目录许可不代表各产品或文件的使用授权。费用、账号、国内访问与版本兼容条件以原始发布者最新说明为准。