证明的技艺

本书讨论如何书写细致而严谨的数学证明。本书配有以计算机形式化语言 Lean 写成的代码。请前往配套的 GitHub 仓库 https://github.com/hrmacbeth/math2001，将这些代码下载到自己的计算机，或在 Gitpod 云端打开。

本书面向大学低年级学生，并为 Fordham University 的 Math 2001 课程而写。若有意见或修正，欢迎联系作者 Heather Macbeth。

• 前言
  • 关于本书
  • 为什么使用 Lean？
  • 内容与预备知识
  • 教师说明
  • 致谢

• 1. 计算式证明
  • 1.1. 证明等式
  • 1.2. 在 Lean 中证明等式
  • 1.3. 提示与技巧
  • 1.4. 证明不等式
  • 1.5. 一种简便写法
• 2. 有结构的证明
  • 2.1. 中间步骤
  • 2.2. 调用引理
  • 2.3. “或”与分类证明
  • 2.4. “且”
  • 2.5. 存在性证明
• 3. 奇偶性与整除性
  • 3.1. 定义；奇偶性
  • 3.2. 整除性
  • 3.3. 模算术：理论
  • 3.4. 模算术：计算
  • 3.5. 贝祖等式
• 4. 有结构的证明（二）
  • 4.1. “对所有”与蕴含
  • 4.2. “当且仅当”
  • 4.3. “存在唯一”
  • 4.4. 矛盾的假设
  • 4.5. 反证法
• 5. 逻辑
  • 5.1. 逻辑等价
  • 5.2. 排中律
  • 5.3. 否定的范式
• 6. 归纳法
  • 6.1. 引言
  • 6.2. 递推关系
  • 6.3. 两步归纳法
  • 6.4. 强归纳法
  • 6.5. 帕斯卡三角形
  • 6.6. 带余除法定理
  • 6.7. 欧几里得算法
• 7. 数论
  • 7.1. 素数有无穷多个
  • 7.2. 高斯引理与欧几里得引理
  • 7.3. 二的平方根
• 8. 函数
  • 8.1. 单射性与满射性
  • 8.2. 双射性
  • 8.3. 函数复合
  • 8.4. 积类型
• 9. 集合
  • 9.1. 引言
  • 9.2. 集合运算
  • 9.3. 集合的类型
• 10. 关系
  • 10.1. 自反、对称、反对称、传递
  • 10.2. 等价关系

附录

• Lean 策略索引
• 过渡到主流 Lean