Stephen Diehl 编写的教程《From Zero to QED》

该教程为读者提供 Lean 4 交互式定理证明器的非正式入门指南。
教程将 Lean 4 拆分为“现代功能编程语言”与“交互式定理证明器”两个维度，通过从基础语法、类型系统到类型论、形式化逻辑以及人工智能交叉领域的循序渐进讲解，让没有定理证明经验的读者能够编写实际程序，更能学会利用计算机进行严谨的数学证明。