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 以内没有临界点」恰好变为所有 。于是反例被打包成圆盘中的两组点：其余零点 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 不等式（而且只需要其可由算术 - 调和平均不等式加归纳推出的特殊情形）