AI + 数学：从入门到参与实战指南

不需要数学博士学位，只需要一点编程逻辑和探索精神。
整理日期：2026-08-16。文末附全部参考链接（注脚格式）。

一、背景：发生了什么？

1. 森多夫猜想（Sendov's Conjecture）是什么？

一句话版本：一个复系数 n 次多项式，如果所有根都落在单位圆盘里，那么每个根附近（距离不超过 1）必然存在至少一个导数的根（临界点）。

• • 1958 年由保加利亚数学家 Blagovest Sendov 提出，表述极简单，却悬而未决近 70 年。
• • 此前只有部分情形被解决。2020 年陶哲轩（Terence Tao）证明了"次数足够大时猜想成立"（sufficiently high degree），但有限次数的情形仍是缺口。
• • 直观理解：根的分布"挤压"了临界点的位置，临界点不会离根太远。

2. 2026 年 8 月的突破时间线

3. 为什么这件事重要？

• • 这是第一次由 AI 深度参与、人类主导、机器严格验证地解决一个公开著名猜想——不是 AI 独立完成的，也不是传统人工证明。
• • 分工模式堪称范本：AI 负责海量探索与繁琐计算，人类负责战略导航，Lean 4 负责无情的逻辑裁判，大师负责消化与提炼。
• • 陶哲轩的精简（9 万行 → 1.5 万行）说明：核心逻辑其实很优雅，9 万行是"AI 草稿"的正常形态。

二、第一步：认识核心武器 —— Lean 4

这次证明的核心不是 AI "算"出来的，而是 AI "写"出来的，再由 Lean 4 这个"超级裁判"逐行验证。

• • 它是什么？ 既是编程语言，也是定理证明器（proof assistant）。用写代码的方式写数学证明：编译器报错 = 证明有逻辑漏洞；编译通过 = 证明成立。
• • 为什么现在学？ 它是 AI 辅助数学研究的事实标准。陶哲轩、Peter Scholze（Liquid Tensor Experiment）、Lech Mazur 都在用；背后是庞大的数学库 Mathlib。
• • 怎么开始？
1. 1. 环境搭建：VS Code + Lean 4 插件，体验最好。写错一步，右边立刻亮红灯，实时反馈。
2. 2. 官方教程：
• • 《Theorem Proving in Lean 4》：入门必读，教你怎么写证明。
• • 《Mathematics in Lean》：进阶，教你怎么把大学数学（分析、代数）翻译成 Lean 代码。
3. 3. 社区：Lean Zulip Chat，全球最活跃的 Lean 社区，陶哲轩本人也在，提问通常很快有回复。

三、第二步：理解"人机协作"的新模式

这次突破最震撼的不是结果，而是过程。可以把它看作一个"超级实习生"的故事：

1. 1. AI 探索（GPT-5.6 Pro）：在海量可能性中"猜"路径，生成代码草稿，处理繁琐计算和不等式放缩。
2. 2. 人类导航（Lech Mazur）：定战略——告诉 AI 往哪个方向证、哪个引理可能有用、别在死胡同里打转。Mazur 同时负责筛选、核对模型输出并撰写论文。
3. 3. 机器验证（Lean 4）：无情的裁判。AI 写错一步，Lean 立刻报错。这保证了 9 万行代码没有一个逻辑漏洞。
4. 4. 大师消化（陶哲轩）：把 9 万行"机器码"精简成 1.5 万行，置于已有文献脉络中，并发现它其实证明了更强的结论。

你的机会

未来的数学家 / 算法工程师，核心竞争力不再是"手算积分"，而是：

• • Prompt Engineering for Math：精准描述数学问题，引导 AI 找到正确引理。
• • Proof Debugging：Lean 报错时，快速判断是 AI 逻辑错了，还是前提设错了。
• • Math Translation：把自然语言的数学直觉，翻译成形式化的 Lean 代码。

四、第三步：现在就能做的 3 件小事

1. 1. 围观"案发现场"
• • 打开 GitHub 仓库 teorth/sendov（陶哲轩消化版），以及 ProofAtlas 上的原始形式化页面。
• • 不用全看懂，看看 theorem sendov_conjecture ... := by 后面的结构，感受一下：原来数学证明长这样。
2. 2. 玩个"数学游戏"
• • 玩 Natural Number Game（基于 Lean 的网页游戏，免安装）。
• • 用归纳法证明 1+1=2，以交互方式理解 Lean 的逻辑。最好的入门方式。
3. 3. 关注 "AI-first" 平台与一手解读
• • ProofAtlas（Lech Mazur 的平台）：证明逐步可视化、带依赖关系图。这是未来数学论文的样子。
• • 陶哲轩博客：读《A digestion of the proof of Sendov's conjecture》。写得非常通俗，是理解"人类如何消化 AI 证明"的最佳教材。

五、避坑指南

• • 别死磕复分析：森多夫猜想用到的复分析工具其实很基础（多项式性质、莫比乌斯变换）。难点在形式化，不在数学本身。
• • 别指望 AI 直接给答案：当前 AI 在长逻辑链上仍会"一本正经地胡说八道"。Lean 4 才是那个不会撒谎的伙伴，AI 只是草稿纸。注意：Lean 形式化证明与论文手稿并非逐行对应，形式化走的是更精简的路线。
• • 别被 9 万行吓到：陶哲轩精简后只有 1.5 万行，核心逻辑很优雅。

六、如果这周只有 1 小时

👉 去玩 Natural Number Game，或者读陶哲轩那篇 Digestion 博客。

比背 100 个公式都管用。

七、参考资料

事件核心资料

• • 陶哲轩博客：A digestion of the proof of Sendov's conjecture^[1]（2026-08-12）
• • 消化版形式化仓库（约 1.5 万行）：teorth/sendov on GitHub^[2]
• • 原始论文与形式化（ProofAtlas）：A Computer-Assisted Proof of Sendov's Conjecture^[3]（2026-08-05）
• • 论文 PDF^[4]
• • 证明候选稿修订记录：ProofAtlas proof candidate (Rev 14)^[5]
• • 第三方报道：Researcher Simplifies AI-Generated Proof of Sendov's Conjecture (hyper.ai)^[6]

背景知识

• • 维基百科：Sendov's conjecture^[7]
• • 陶哲轩 2020 年高次数情形论文：arXiv:2012.04125^[8]

Lean 4 学习资源

• • 入门游戏：Natural Number Game^[9]（免安装，浏览器直接玩）
• • 入门教材：Theorem Proving in Lean 4^[10]
• • 进阶教材：Mathematics in Lean^[11]
• • 环境搭建：Lean 4 Quickstart（VS Code + 插件）^[12]
• • 数学库：Mathlib4^[13]
• • 社区：Lean Zulip Chat^[14]

1. https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/↩︎
2. https://github.com/teorth/sendov↩︎
3. https://proofatlas.ai/formalizations/sendov-conjecture/↩︎
4. https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf↩︎
5. https://proofatlas.ai/research/sendov-conjecture-proof-candidate/↩︎
6. https://hyper.ai/en/stories/2151971ca8a6d993ce56e176696db431↩︎
7. https://en.wikipedia.org/wiki/Sendov%27s_conjecture↩︎
8. https://arxiv.org/abs/2012.04125↩︎
9. https://adam.math.hhu.de/#/g/leanprover-community/nng4↩︎
10. https://leanprover.github.io/theorem_proving_in_lean4/↩︎
11. https://leanprover-community.github.io/mathematics_in_lean/↩︎
12. https://leanprover.github.io/lean4/doc/quickstart.html↩︎
13. https://github.com/leanprover-community/mathlib4↩︎
14. https://leanprover.zulipchat.com/↩︎