Lean 4 定理证明

作者：Jeremy Avigad, Leonardo de Moura, Soonho Kong and Sebastian Ullrich, 以及Lean社区 译者 subfish_zhou

原文地址Theorem Proving in Lean 4

本中文教程旨在教你使用Lean 4。 参考Lean 4 Manual中的Setting Up Lean section一节来安装Lean。本项目也包括一个快速安装教程。 本书的Lean 2 和Lean 3 版本见这里。

本项目的翻译量较大，因此大多采用机翻，仅供习惯中文的读者作为参考，译者推荐有能力的读者阅读原文。欢迎对本译文提出宝贵意见，可邮件至subfishzhou@gmail.com 译者自制的习题参考答案在本项目Github仓库的Exercise文件夹中。本项目尚未完工。