随着人工智能推理能力迎来井喷式发展，数学研究正在经历一场深刻变革。那些曾经困扰人类数十年的未解难题，正在 AI 的辅助下加速解决。这不，又一个困扰了数学界约 70 年的难题——森多夫猜想，在一位名叫 Lech Mazur 的初创科技公司 CEO 的协助下，借助 AI 被攻克了。
证明论文题为《计算机辅助证明森多夫猜想》，作者 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 的临界点？这个猜想的背景来自经典的高斯 – 卢卡斯定理（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 以内没有临界点”恰好变为所有 q_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。
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 能证明定理了，但远未结束。被解决的问题打开的往往是更多的问题。