1.6 KiB
1.6 KiB
title, created, updated, type, tags, sources
| title | created | updated | type | tags | sources | |||||
|---|---|---|---|---|---|---|---|---|---|---|
| Lean 证明助手（Lean Proof Assistant） | 2026-07-03 | 2026-07-03 | concept |
|
|
Lean 证明助手
一个基于依赖类型理论的交互式定理证明器和函数式编程语言，由 Leonardo de Moura 等开发。
核心定义
Lean 是现代 formal-theorem-proving 中最活跃的系统之一。它同时是一门函数式编程语言和一个证明助手，允许数学家编写机器可检查的证明，由严格的 Lean 内核验证。
关键特性
- 依赖类型系统：类型可以依赖值，使证明即程序（Curry-Howard 同构）
- mathlib4：庞大的数学形式化库
- Lean Blueprint 工具：用于组织大型形式化项目的人类可读路线图 + DAG 可视化
- 验证保证：Lean 编译器提供严格的语法和类型检查
在 ATP 中的作用
在 leap-agentic-atp 等 agentic 框架中，Lean 编译器扮演双重角色：
- 形式验证器：检查候选证明的正确性
- 反馈源：编译错误信息指导 LLM 的迭代修正
Lean 的 sorry 占位符机制允许部分证明（sketch）——声明子目标而不必立即证明——这是 blueprint-driven-atp 的关键能力。
大型项目
- Fermat's Last Theorem 形式化路线图（多年代码，显式依赖图）
- mathlib4 社区驱动的数学知识库