教材大纲：《给非数学专业人士 Lean 4 速成课》

目标读者：“金色葡萄”——（一位好奇心驱动、有编程基础、数学停留在中学和基础微积分的理工科专业人士）

核心承诺 (A点 -> B点)：

• A点：您听说过 Lean 4，但望而生畏，因为它的学习曲线总是和高等数学的悬崖峭壁绑定在一起。
• B点：本书将彻底分离“工具”与“数学”。学完后，您将能熟练使用 Lean 4 工具本身，并有绝对的信心，借助 AI + Lean 4 去攻克您专业领域的高等数学问题。

第一部分：出发！——“你好，证明”

• 本部分目标：解决“金色葡萄”的“启动恐惧”。我们要以最快的速度，让他获得第一次成功的“Wow!”时刻。

第 1 章：为什么是 Lean？为什么是你？

• 挂钩：“陶哲轩也用它！”——这不只是数学家的玩具，这是（未来）所有科学家的新计算器。
• 论点：学习 Lean 4 最大的障碍是“认知失调”——用研究生级别的工具去证明 $1+1=2$。
• 本书的前提：我们将彻底规避这个陷阱。我们将使用您最熟悉的“中学数学”作为练习场，把所有精力集中在“工具”上。
• 着陆：您将看到，证明 $(a+b)^2$ 和证明“黎曼猜想”（的某一步）在 Lean 4 中使用的是完全相同的思维模式。

第 2 章：搭建你的“证明实验室”

• 挂钩：对于您（“金色葡萄”）这样的程序员，最好的类比是：VS Code 是您的 IDE，Lean 4 是您的“实时编译器”。
• 论点：一个顺滑的环境是快乐学习的开始。
• 支持：
  • 一步步安装：VS Code、Lean 4 插件、lake (Lean 的项目管理器)。
  • 创建您的第一个 lake 项目。
  • 认识您的新“副驾驶”——“Infoview”窗口（信息视图）。
• 着陆：当您的 Infoview 窗口中跳出“Goals accomplished! 🎉”时，您的实验室就搭建完毕了。

第 3 章：你的第一个证明：$2+2=4$

• 挂钩：在 Lean 4 中，证明 $2+2=4$ 和证明 $2+2=5$ 有什么区别？
• 论点：Lean 4 是一个“对话式”证明器。您的工作不是“写代码”，而是和 Lean 4 “聊天”，直到您的“目标”（Goal）消失。
• 支持：
  • example : 2 + 2 = 4 := by ...
  • 第一个策略！refl (自反性)。
  • Infoview 体验：亲眼看着“目标”从 2 + 2 = 4 变成 4 = 4，最后被 refl 消灭。
• 着陆：恭喜！您刚刚完成了您的第一个数学证明。这比您想象的简单，不是吗？

第二部分：Lean 4 的“世界观”

• 本部分目标：解决“金色葡萄”的“理论心魔”。“这东西看起来太怪了，它到底是什么？” 我们用“类比”来战胜它。

第 4 章：“命题”即“类型”

• 挂钩：Lean 4 最核心，也是最“怪异”的思想。
• 论点：在 Lean 4 中，“证明一个命题”就等于“构造一个该类型的实例”。
• 类比：
  • Type (类型) 就像是“名词”：Nat (自然数), Real (实数)。
  • Prop (命题) 就像是“挑战”：“$2+2=4$” (一个挑战), “$a>b$” (另一个挑战)。
  • 一个“证明” (Proof) 就像是“完成了挑战的凭证”：您手里有这个凭证，Lean 4 就相信您。
• 着陆：def (定义函数) 和 theorem (定义定理) 的区别。

第 5 章：定义你自己的“中学世界”

• 挂钩：还记得中学函数 $f(x) = x^2$ 吗？我们怎么在 Lean 4 里“写”出它？
• 论点：学习如何用 def 和 theorem 来描述我们的中学数学世界。
• 支持：
  • def square (x : Real) : Real := x * x (定义函数)
  • theorem square_positive (x : Real) : square x ≥ 0 := by ... (陈述定理)
  • Prop 上的连接词 (逻辑连接): ∧ (并且), ∨ (或者), → (如果...那么...), ¬ (不是)。
• 着陆：您现在可以用 Lean 4 的语言，“翻译”您作业本上的任何一道数学题了。

第三部分：Lean 4 的“策略工具箱”

• 本部分目标：解决“中段乏力”。“金色葡萄”会卡住：“我盯着目标，但不知道该用什么工具？” 我们将策略 (Tactics) “工具化”、“拟人化”。

第 6 章：“替换”的艺术：rw (Rewrite)

• 挂钩：中学代数的核心就是“代换”。rw 就是您在草稿纸上画的“等于号箭头”。
• 论点：rw 是 Lean 4 中最常用、最强大的“手动工具”。
• 支持：theorem add_comm (a b : Real) : a + b = b + a := by ...
• 实战：证明 (x + y) + z = z + (y + x)。您将学会如何用 rw [add_comm] 来“重写”您的目标。

第 7 章：“如果...那么...”：intro 和 apply

• 挂钩：“如果 $x=4$，那么 $x+1=5$”。这在 Lean 4 里怎么说？
• 论点：如何处理带“如果...”的命题 (→)，以及如何使用您的“假设” (Hypothesis)。
• 支持：
  • theorem ex1 (x : Real) (h : x = 4) : x + 1 = 5 := by ... (h 是你的假设)。
  • 使用 rw [h] 来消费假设。
  • 使用 intro h 来引入假设。
• 着陆：您现在掌握了数学推理的“基本步法”。

第 8 章：“自动清洁工”：simp

• 挂钩：“我不想一步一步 rw 了，太累了！”
• 论点：simp 是您的第一个“自动化”伙伴。它会（基于一个规则库）自动帮您完成所有“显而易见”的代换。
• 支持：
  example (x y : Real) : (x + y) - y = x := by simp
• 着陆：您的第一个“半自动”证明。simp 会是您最好的朋友，有时也会是您最抓狂的敌人。

第四部分：“称霸”中学练习册（实战）

• 本部分目标：交付本书的核心价值！“金色葡萄”将在这里获得巨大的“Aha!”时刻，彻底爱上 Lean 4。

第 9 章：解锁“无限军火库”：导入 Mathlib

• 挂钩：到目前为止，我们都在“真空”中。现在，我们站在巨人的肩膀上。
• 论点：Mathlib 是 Lean 4 庞大的、世界顶级的数学库。导入它，您就拥有了成千上万条已证实的定理。
• 支持：import Mathlib.Data.Real.Basic
• 着陆：“金色葡萄”熟悉的编程类比：import Mathlib 就像 import numpy as np。

第 10 章：“代数恒等式”终结者：ring

• 挂钩（“Wow!”时刻）：证明 $(a+b)^2 = a^2 + 2ab + b^2$。
• 论点：ring 策略是一个“超级专家”。它可以自动证明任何在“交换环”（如实数）中成立的多项式等式。
• 支持：
  example (a b : Real) : (a + b)^2 = a^2 + 2 * a * b + b^2 := by ring
  是的，就这一行。
  example (a b : Real) : (a - b) * (a + b) = a^2 - b^2 := by ring
  平方差公式，搞定。
• 着陆：这就是我们隔离工具和数学的原因！您不需要知道 ring 是怎么实现的，您只需要知道在中学代数中，何时使用它。

第 11 章：“不等式”终结者：linarith

• 挂钩：“如果 $a > b$ 且 $b > c$，那么 $a > c$”。
• 论点：linarith (Linear Arithmetic) 是另一个“超级专家”，自动解决所有线性不等式。
• 支持：
  example (a b c : Real) (h1 : a > b) (h2 : b > c) : a > c := by linarith
  中学作业题：
  example (x : Real) (h : 2*x + 5 < 11) : x < 3 := by linarith
• 着陆：您的两个“王牌”策略在手，90%的中学代数恒等式和不等式已经被您“秒杀”了。

第 12 章：综合演练：解“二元一次方程组”

• 挂钩：还记得中学的“代入消元法”吗？
• 论点：没有一个策略能“包打天下”。真正的力量在于“组合”它们。
• 支持：
  example (x y : Real) (h1 : 2*x + 3*y = 7) (h2 : x - y = 1) : x = 2 ∧ y = 1 := by ...
  我们将在这里“编排”一场战术胜利：用 intro h1 h2，从 h2 中 rw，最后用 linarith 收尾。
• 着陆：您现在不再是一个“使用者”，您是一个“指挥家”。

第 13 章：实战“Boss”：证明“等比数列”求和公式

• 挂钩：证明 $1 + q + ... + q^n = \frac{1 - q^{n+1}}{1 - q}$ (当 $q \neq 1$)
• 论点：这是我们第一次接触“数学归纳法” (induction)。
• 支持：我们将展示如何使用 Mathlib 中已有的 sum (求和) 符号和 induction 策略来“组合”出一个漂亮的证明。
• 着陆：恭喜！您刚刚完成了一个“大学级别”的证明（归纳法），但用的仍然是您最熟悉的“中学素材”。

第五部分：飞跃！——你的 B 点

• 本部分目标：赋权“金色葡萄”去行动。您已经准备好了。

第 14 章：B 点观光：如何“读懂”微积分

• 挂钩：您是对的，极限和级数是中学数学的“最后一公里”。
• 论点：我们在前面（第13章）已经学会了如何代数地处理级数。现在，我们来看看 Lean 4 是如何分析地描述它们的（即“收敛性”）。
• “读代码”：
  • 展示 Mathlib 中“数列极限”(Tendsto) 的定义。
  • 展示 Mathlib 中“导数”(DifferentiableAt) 的定义。
• 着陆：您可能还不能证明它，但您现在已经能看懂高等数学在 Lean 4 中的“源代码”了。这不再是“天书”，它只是我们已学工具（def, theorem, →）的组合。

第 15 章：您的新伙伴：“AI + Lean 4”

• 挂钩：陶哲轩的秘密武器，也是您的。
• 论点：AI (Gemini, ChatGPT) 目前是“不完美”的 Lean 4 程序员。但“不完美”正是您的机会。
• 类比：
  • AI 是您“笨拙但博学的实习生”。它会生成 90% 会报错的代码。
  • 您是“高级审查员”。利用本书所学，您现在是 AI 的 Code Reviewer。您能看懂 AI 的错误，并修复它们。
• 着陆：这就是最前沿的“AI 辅助证明”工作流。

第 16 章：您已“B点”：成为“Lean 4 侦探”

• 挂钩：这不是结束，而是开始。
• 论点：您已经完成了从 A点 到 B点 的转变。您不再是“学习者”，您已经是“使用者”和“侦探”。
• 赋权 (行动号召)：
  • 您在 Mathlib 中迷路时该怎么办？(如何使用文档)
  • 您遇到问题时该去哪里？(Lean 4 Zulip 社区)
• 最后的着陆：去吧，用 Lean 4 和 AI 解决一个您专业领域（例如，生物统计、药物模型）中的小问题。您已经准备好了。