电子书《Mathematics in Lean》
leanprover-community.github.io/mathematics_in_lean/index.html
“本书的目标是教你如何使用 Lean 4 交互式证明助手来将数学形式化。它假定你了解一些数学知识，但要求不高。尽管我们将涵盖从数论到测度论和分析等领域的例子，但我们将重点关注这些领域的基础方面，希望即使你对这些内容不熟悉，也能在学习过程中逐步掌握。我们也不预设你有任何形式化方法的背景知识。形式化可以被视为一种计算机编程：我们将用一种像编程语言一样规范化的语言来书写数学定义、定理和证明，以便 Lean 能够理解。作为回报，Lean 会提供反馈和信息，解释表达式并确保其格式正确，并最终证明我们证明的正确性。”
AI创造营
