AI + 陶哲轩把 70 年的森多夫猜想一次性画上句号 —— 一个隐藏的更强结果也一并被解决
2026 年 8 月初，初创公司 ProofAtlas 创始人 Lech Mazur 在 GPT-5.6 Pro 的辅助下完成了森多夫猜想（Sendov's Conjecture）的证明论文，配有约 9 万行 Lean 4 形式化代码。8 月 12 日，菲尔兹奖得主陶哲轩在博客发文，说自己花了数日（同样在大量 AI 辅助下）将这份证明消化、简化并重新形式化，把 Lean 代码压缩到约 1.5 万行——而更关键的是，他发现整理后的论证实际证明了一个更强的命题，1972 年提出的 Phelps-Rodriguez 猜想随之被一并解决。复分析领域最著名的公开问题之一，在 AI 参与下一次画上了句号。
一、森多夫猜想：一个优雅到令人沮丧的问题
森多夫猜想由保加利亚数学家 Blagovest Sendov 于 1958 年前后提出，陈述极简：
设 p(z) 是一个 n 次复多项式（n ≥ 2），其所有零点都在闭单位圆盘内（即 |z| ≤ 1）。那么，对 p 的任意零点 a，至少存在一个临界点 w（即导数 p'(z) 的零点），使得 |w − a| ≤ 1。
换种说法：如果一个复系数多项式的所有根都位于单位圆内，那么每一个根附近，是否一定存在一个距离不超过 1 的临界点？
这个猜想的背景来自经典的高斯-卢卡斯定理（Gauss-Lucas theorem）：多项式的所有临界点都落在其零点构成的凸包内部——这是一个整体性结论，而森多夫猜想问的则是局部版本。
极端例子 p(z) = zⁿ − 1：零点是单位根，唯一临界点是原点（重数 n−1），距离恰好等于 1。这说明常数 1 是紧的——不能再改进。
二、68 年的接力
数学界围绕这条猜想已经跑了 68 年：
| 年份 | 进展 |
|---|---|
| 1969 | Meir 与 Sharma 证明 n < 6 |
| 1991 | Brown 推进到 n < 7 |
| 1996 | Borcea 推进到 n < 8 |
| 1999 | Brown 与 Xiang 推进到 n < 9——之后超过 20 年没有低次推进 |
| 2020 | 陶哲轩证明「n 充分大」情形（无显式上界），刊于《Acta Mathematica》 |
| 2026 年初 | 张腾（Teng Zhang）把陶哲轩的"充分大"显式化到 n 高达 10²⁰⁰⁰⁰⁰ |
| 2026 年 8 月 5 日 | Lech Mazur 用 GPT-5.6 Pro 生成证明，配 9 万行 Lean 4 代码 |
| 2026 年 8 月 12 日 | 陶哲轩消化、简化证明至 1.5 万行 Lean 代码，并发现 Phelps-Rodriguez 猜想随之成立 |
提出 Sendov 猜想的数学家、当时还在读博的研究者本人，17 年未能突破，最终由 AI 组合完成了关键证明。这是数学史上「AI 把一道长期悬而未决的经典难题」在公开同行评议机制下完整跑通的少数案例之一。
四、为什么 Phelps-Rodriguez 是更强的命题
陶哲轩消化后的论证实际上证明了所谓 Conjecture 3（Sendov 内部形式）：
设 n ≥ 2。令 p 是一个 n 次多项式，所有零点都在单位圆盘内。那么如果 a 是 p 的零点，存在 p 的临界点 w 使得 |w − a| < 1。
这直接蕴含了 Phelps-Rodriguez 猜想（1972 年提出）：要求距离严格小于 1，除非 a 落在单位圆上且 p 是 zⁿ − aⁿ 的标量倍数。换句话说，68 年前 Sendov 问的是「距离 ≤ 1 够不够」，陶哲轩版本的消化直接给出了「距离 < 1 几乎一定可以」，更强、更细、且对历史上的极端例子保持紧致。
四、证明思路的「令人惊讶地初等」
陶哲轩对这份证明给了颇高评价：「证明过程令人惊讶地初等——除了代数基本定理与莫比乌斯变换的基本性质之外，几乎没有用到任何复分析工具；论证中所需的最深不等式，也仅仅是麦克劳林不等式的一个特殊情形。」
骨架可以概括为反证法的四步：
- 归一化：把反例旋转，使零点 a 落在 [0,1) 上；把临界点 wⱼ 换成倒数坐标 qⱼ = 1/(a − wⱼ)，把"距离大于 1"的反例条件翻译成两个在单位圆盘内的点集（剩余零点和倒数临界点）
- 沟通恒等式：通过在自然点上对 p 和 p′ 求值，推导出四个代数关系——质心恒等式、极化恒等式、两个原点恒等式——把零点集和临界点集的质心联系起来
- 消除多项式：把四个恒等式与单位圆盘内点集的条件一起处理，导出矛盾——这里多项式 p 本身不出现
- 分支分析：极化恒等式 + 莫比乌斯变换估计给出关键积分下界，这是 a 必须为实数的唯一一处
低次情形（n ≤ 5）通过逐项分析积分直接导出矛盾；高次情形（n ≥ 5）则用两个不等式——极化不等式（AM-GM 放松积分）和原点不等式（来自第一、第二原点恒等式 + 质心恒等式）——约束可行区域。n ≥ 101 时两可行区域解析不交；5 ≤ n ≤ 100 用精确有理数构造的 Bernstein 多项式证书做数值验证，全程由 Lean 系统检验。
五、人机协作的新范式
这件事折射出的意义早已超越了森多夫猜想本身：
第一层是证明者身份的改变。 马祖尔并非职业数学家，却凭借 AI 工具的辅助攻克了困扰专业学者数十年的经典难题。提出"Tang-Zhang 猜想"的张腾（Teng Zhang）得知消息后感慨：「森多夫猜想是我博士期间的研究课题，如今它被 AI 解决了，我的青春就此结束了。」
第二层是协作模式的浮现。 马祖尔借助 AI 生成证明并完成形式化验证 → 陶哲轩再次借助 AI 辅助完成消化、简化与重新形式化 → 全过程在 Lean 类型检查器下可被机器严格核验。AI 在这一过程中既是探索工具，也是验证工具；人类数学家的角色则逐渐转向判断、提炼与联结。
第三层是形式化验证成为信任基础。 在传统数学研究中，一份证明的可信度高度依赖同行评审机制；而 Lean 这类形式化验证工具提供了另一条平行的信任路径——只要类型检查器顺利通过，证明中的每一步逻辑都经过了严格核验。这对由 AI 生成的证明而言尤其关键。
陶哲轩在博文末尾坦言，包括 Borcea 猜想、Schmeisser 猜想以及 Smale 问题在内的多个相关猜想依然悬而未决——他"确实尝试过用 AI 工具攻击这些问题，但尚未取得显著成功"。也就是说，这条新范式不是万能钥匙，而是一条新走出来的、确实走得通的路径。
形式化代码已在 GitHub 开源：github.com/teorth/sendov。
来源
讨论回复
加载中...正在加载回复...
推荐
智谱 GLM-5 已上线
我正在智谱大模型开放平台 BigModel.cn 上打造 AI 应用，智谱新一代旗舰模型 GLM-5 已上线，在推理、代码、智能体综合能力达到开源模型 SOTA 水平。