Lean 4 定理证明 作者：Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, 以及来自 Lean 社区的贡献者 Lean-zh 项目组 译 本书假定你使用 Lean 4。安装方式参见 Lean 4 手册 中的 快速开始 一节。 本书的第一版为 Lean 2 编写，Lean 3 版请访问 此处。