随着 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 以内没有临界点」恰好变为所有
。于是反例被打包成圆盘中的两组点：其余零点 z_j 和倒数临界点 q_j。
第二步：建立「通讯恒等式」。 陶哲轩将核心的四条关系称为 communication identities：质心恒等式（零点质心 = 临界点质心）、极化恒等式、第一原点恒等式、第二原点恒等式。这些恒等式通过在几个自然位置求值多项式 p 及其导数得出。
此后出现了一个意外的转折：多项式 p 本身不再出场。 矛盾完全从「两组点都在单位圆盘内」加上这四条恒等式推出。
第三步：分支点。 极化恒等式结合 Möbius 变换的估计
，导出一个关键的积分下界：
这是整个论证唯一用到 a 为实数的地方，也是此后论证分叉的起点。
低次数（n ≤ 5） 在此直接结束：用标量 X (t) = a + (1-a^2) t 控制被积函数的每一项，得到的积分
在 0 < a < 1、m ≤ 4 时严格小于 1，与上述下界直接矛盾。
高次数（n ≥ 5） 则需要同时建立两个不等式。一个是从上述积分经 AM-GM 不等式松弛得到的「极化不等式」，另一个是从第一、第二原点恒等式结合质心恒等式推出的「原点不等式」。
两个不等式对核心参数（q_j 均值的实部 x 和参数
划定的可行域互不相容。对 n ≥ 101 的情形，可以解析地证明两个不等式不可能同时成立；5 ≤ n ≤ 100 的区间则用精确有理数的 Bernstein 多项式证书完成数值验证，全程由 Lean 检验。
边界情形（|a|=1） 虽由 Rubinstein 早已解决，但陶哲轩用同一套框架给出了新证明。
此时极化恒等式退化（因为 1-a^2=0），改用 Meir-Sharma 恒等式。由此得到 
，再结合
的半平面界，逐项强制 q_j = 1，从而推出 p 必须是
的形式。这一分析精确刻画了等号成立的条件，正是 Phelps-Rodriguez 猜想中需要排除的极端情形。
陶哲轩的评价是：「证明令人惊讶地初等。除了代数基本定理和 Möbius 变换的基本性质外，没有用到任何复分析工具；最深的不等式输入只是 Maclaurin 不等式（而且只需要其可由算术 - 调和平均不等式加归纳推出的特殊情形）。」
陶哲轩消化的一个关键发现是：整理后的论证实际上证明了比森多夫猜想更强的「内部形式」。
Phelps-Rodriguez 猜想（1972）在森多夫猜想的基础上要求距离严格小于 1，除非 a 在单位圆周上且 p 是 z^n - a^n 的标量倍。由于证明的边界情形分析精确刻画了等号成立的条件，这个更强猜想作为推论直接得出。
陶哲轩将整个论证重新形式化为约 1.5 万行 Lean 代码，已开源在 GitHub。
开源链接：github.com/teorth/sendov
AI 在数学中的角色正在改变
第一，证明者的身份。Lech Mazur 不是职业数学家，但借助 AI 工具完成了困扰专业学者数十年的问题。正如知乎上 Tang-Zhang 猜想提出者之一 Teng Zhang 的感慨：「Sendov 猜想是我博士期间的课题，它被用 AI 解决了，我的青春结束了。」
第二，人机协作的模式。Mazur 用 AI 生成证明并形式化验证（9 万行 Lean），陶哲轩再用 AI 辅助消化、简化和重新形式化（1.5 万行 Lean）。AI 既是探索工具也是验证工具，人类数学家的角色转向判断、提炼和联结。
第三，形式化验证的信任基础。在传统数学中，一份证明的可信度依赖同行评审。Lean 形式化提供了另一种信任路径：如果类型检查器通过了，证明中的每一步都是逻辑上严格的。对于 AI 生成的证明，这一点格外重要。
陶哲轩在博文末尾列出了仍然开放的相关猜想，包括 Borcea 猜想、Schmeisser 猜想和 Smale 问题，并坦言「我确实也尝试用 AI 工具攻击这些问题，但没有取得显著成功」。
AI 能证明定理了，但远未结束。被解决的问题打开的往往是更多的问题。
© THE END
转载请联系本公众号获得授权
投稿或寻求报道：liyazhou@jiqizhixin.com
