Study note
Theorem Proving in Lean 4
Properties
- Type
- Books
- Status
- 想读
- Domain
- Compilers / PL
- Category
- 类型系统、形式化与定理证明
- Source
- lean-lang.org
- Vault note
library/books/compilers/Theorem-Proving-in-Lean-4-352cc3250b2434ec.md
Summary
Lean 4 定理证明官方教材，覆盖依赖类型论、命题与证明、量词与等式、tactic、与 Lean 交互、归纳类型、归纳与递归、结构/记录、类型类、conversion tactic mode、axioms and computation。
Highlights
适合系统学习 Lean 作为证明助手的核心机制，是进入形式化数学、程序验证和依赖类型证明的主入口。
Notes
Jeremy Avigad、Leonardo de Moura、Soonho Kong、Sebastian Ullrich。
Comments
Loading comments...