Lean 语言参考手册
这是 Lean 语言参考手册 的中文版本。
它旨在全面、精确地描述 Lean，供用户查阅详细信息，而不是作为面向新用户的入门教程。
其他中文资料请参阅 Lean 中文社区；英文资料请参阅 Lean 文档总览。
本手册涵盖 Lean 4.34.0-rc1 版本。
Lean 是一种基于依值类型论的交互式定理证明器，既可用于前沿数学，也可用于软件验证。 Lean 的核心类型论足以表达非常复杂的数学对象，同时又足够精简，可以有独立实现，从而降低影响可靠性的缺陷风险。 核心类型论由最小化的内核实现；内核只负责检查证明项。 高级自动化通过富有表现力的策略语言支持核心理论与内核。 每个策略都会产生由内核检查的核心证明项，因此策略中的缺陷不会危及 Lean 整体的可靠性。 和 Lean 的许多其他部分一样，策略语言可由用户扩展，以满足具体形式化项目的需求。 策略本身用 Lean 编写，定义后即可立即使用，无需重建证明器或加载外部模块。
Lean 同时也是一种纯函数式编程语言，其运行时基于引用计数，能够高效处理紧凑数组、多线程及单子式 IO。
作为一门编程语言，Lean 的语言服务器、构建工具、精译器和策略系统等主要组件都由 Lean 自身实现。
本手册使用 Verso 编写；Verso 也是用 Lean 实现的文档创作工具。
即使主要目标是编写证明，熟悉 Lean 的编程功能也很有价值，因为新的策略和证明自动化均由 Lean 程序实现。 因此，本参考手册将 Lean 的证明语言与编程语言两方面结合描述，使二者相互阐明。