【Lean 4 教程】从入门到精通：依赖类型理论与定理证明实战指南
摘要：本文基于 Lean 4.26.0 版本，系统介绍了 Lean 作为编程语言、定理证明器和元编程工具的核心概念。内容涵盖依赖类型理论、命题即类型、策略模式、归纳类型及类型类等高级主题，旨在帮助开发者快速掌握形式化数学与函数式编程的结合之道。
作者：Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich (原著) | 整理：CSDN 社区 适用版本：Lean 4.26.0+
📖 目录
1. 引言：计算与定理证明
形式化数学涉及使用精确的符号语言和规则来表述数学陈述和证明。Lean 是一种依赖类型理论的实例，它既可以作为编程语言，也可以作为逻辑系统，使我们能够编写程序并证明它们满足其规范。
Lean 的三大设计目标
- 🚀 作为编程语言：编写高效、可执行的函数式程序。
- 🛡️ 作为定理证明器：形式化数学并验证证明的正确性。
- 🤖 作为元编程工具：编写程序来生成程序或证明（Meta-programming）。
核心概念预览
- 依赖类型理论：类型可以依赖于值（例如 Vector α n 表示长度为 n 的向量）。
- 命题即类型 (Propositions as Types)：一个命题就是一个类型，该命题的证明就是这个类型的项（柯里 – 霍华德同构）。
- 证明即程序：证明和程序使用相同的语言编写。
— 证明：对于任何命题 p，p → p 成立
theorem idempotent (p : Prop) : p → p :=
fun hp : p => hp
这里 fun hp : p => hp 是一个函数，它接受一个 p 的证明 hp，并返回 hp 本身。
Lean 系统组件
- 内核 (Kernel)：小型、可信任的类型检查器。
- Elaborator (细化器)：将用户友好的语法转换为内核形式。
- 策略 (Tactic
