AI宣布森多夫猜想告破！陶哲轩发现它隐藏的更强结果
编辑｜冷猫
随着 AI 推理能力迎来井喷式的发展，数学研究正在经历一场深刻变化。那些曾经困扰人类数十年的未解难题，正在 AI 的辅助下加速解决。
这不，又有一个至今约 70 年的数学猜想：森多夫猜想，被一位名叫 Lech Mazur 的初创科技公司 CEO，借助 AI 完成了证明。
证明论文题为「A Computer-Assisted Proof of Sendov's Conjecture」，作者 Lech Mazur 宣布：森多夫猜想对所有次数 n≥2 成立， 证明在 GPT-5.6 Pro 辅助下完成 ，配有约 9 万行 Lean 4 形式化代码。
论文链接：https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf
8 月 12 日，陶哲轩在博客发文，称自己花了数天时间（同样在大量 AI 辅助下）将这份证明消化、简化并重新形式化，新版 Lean 代码缩减到约 1.5 万行。
博客链接：https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/
更关键的是，他发现整理后的论证实际上证明了一个更强的命题，1972 年提出的 Phelps-Rodriguez 猜想也随之被解决。
这意味着，复分析领域最著名的公开问题之一，在 AI 的参与下一次性画上了句号。
森多夫猜想：
一个优雅到令人沮丧的问题
森多夫猜想由保加利亚数学家 Blagovest Sendov 于 1958 年前后提出，陈述极其简洁：
设 p (z) 是一个 n 次复多项式（n≥2），其所有零点都在闭单位圆盘内（即 |z|≤1）。那么，对 p 的任意零点 a，至少存在一个临界点 w（即导数 p'(z) 的零点），使得 |w - a| ≤ 1。
换一种说法：如果一个复系数多项式的所有根都位于单位圆内，那么每一个根附近，是否一定存在一个距离不超过 1 的临界点？
示意图由 AI 生成 这个猜想的背景来自经典的高斯 - 卢卡斯定理（Gauss-Lucas theorem）。该定理说：多项式的所有临界点都落在其零点构成的凸包内部。这是一个整体性结论，而森多夫猜想问的则是局部版本。
一个直观的物理图像有助于理解：把零点想象成平面上的电荷，临界点可以类比为这些电荷产生的平衡点。高斯 - 卢卡斯定理说平衡点不会跑出电荷围成的区域，森多夫猜想则说每个电荷的「一步之内」必有平衡点。
猜想中的常数 1 是不可改进的。考虑多项式 p (z) = z^n - 1，其零点是 n 个单位根，唯一的临界点是 n-1 重的原点，每个零点到最近临界点的距离恰好等于 1。这个例子，也正是更强的 Phelps-Rodriguez 猜想必须将 |a|=1 且 p 是 z^n - a^n 的倍数这一族排除在外的原因。
这两个猜想在 a=1 情形下都已得到证实，因此可以将其限制在 0≤a≤1 情形下。这两个猜想均可由此得出：
尽管陈述简洁，森多夫猜想的证明进度却极为缓慢：
1969 年，Meir 和 Sharma 证明 n<6 的情形
1991 年，Brown 推进到 n<7
1996 年，Borcea 推进到 n<8
1999 年，Brown 和 Xiang 推进到 n<9，此后 20 多年再无低次数进展
2020 年，陶哲轩在 Acta Mathematica 上证明「充分大的 n」成立，但论证使用了解析延拓等定性工具，无法给出显式的次数阈值
2026 年初，华人数学家 Teng Zhang（Tang-Zhang 猜想的提出者之一）将陶哲轩的阈值显式化到 10^200000
Lech Mazur 并非学术界的职业数学家。他是一家创业公司的创始人兼 CEO，同时也是 ProofAtlas 平台的创建者，该平台定位为「AI-first formal mathematics」，将可视化解释、形式化陈述、完整源码、依赖关系和反驳路径汇聚在一张不断生长的证据图谱中。
按论文自身的说明， AI 参与的环节包括数学探索、证明发展、测试和审查 。最终产出的 Lean 4 形式化代码约 9 万行。
证明思路到更强猜想
陶哲轩在博客中对证明进行了完整的消化和重组。他说：这种消化带来的一个结果是，该论证实际上证明了猜想 3 ，从而在完全普遍意义上解决了 Sendov 猜想和 Phelps-Rodriguez 猜想。
整个论证走反证法。
核心设定 ： 假设存在反例。设 n 次多项式 p 的零点都在闭单位圆盘内，但存在某个零点 a，其距离 1 以内没有任何临界点。
第一步：归一化 。 通过旋转，将 a 变为 [0,1) 区间上的实数。再将临界点 w_j 改写为倒数坐标 q_j = 1/(a - w_j)。「距离 1 以内没有临界点」恰好变为所有