Lean 4 自动化内幕

 Lean 4 自动化内幕🔗

Ziyu Zhou (子鱼)

本书深入讲解 Lean 4 的自动化（tactic）系统内幕：元编程模型、表达式操作、tactic 实现原理，以及 Mathlib 中各种自动化工具的工作机制。

本书假设你已有基本的 Lean 4 使用经验，了解 theorem、by、simp 等基础语法。

本书校验版本：Lean 4 v4.30.0-rc1，Mathlib 同期主线（2026 年 4 月）。

Contents

  1. 1. 环境与运行约定
  2. 2. Lean 4 元编程模型
  3. 3. Expr：Lean 4 的内部表示
  4. 4. 编写你的第一个 Tactic
  5. 5. 目标管理
  6. 6. Type Class Synthesis
  7. 7. simp——化简的瑞士军刀
  8. 8. ring 和 ring_nf：代数范式化
  9. 9. omega：Presburger 算术决策过程
  10. 10. linarith、nlinarith 与 polyrith
  11. 11. norm_num：数值计算框架
  12. 12. aesop：可配置的启发式搜索
  13. 13. grind：E-matching 与 Congruence Closure
  14. 14. decide 与 native_decide：有限计算判定
  15. 15. positivity：符号非负性推理
  16. 16. fun_prop：函数性质的自动证明
  17. 17. gcongr：广义合同性
  18. 18. field_simp：分式化简
  19. 19. pushneg、contrapose、bycontra
  20. 20. 设计你自己的领域自动化
  21. 21. 反射证明模式
  22. 22. 性能工程
  23. 23. 对接外部工具
  24. 24. 从证明模式到自动化：方法论
  25. 25. 迈向分析自动化
  26. 26. 附录 A：Metaprogramming API 速查表