文章总结： 研究者借GPT-5.6Pro完成近70年数学难题森多夫猜想的证明。陶哲轩用AI辅助重构该证明，发现其同时解决了更强的Phelps-Rodriguez猜想。此事件标志着数学研究范式的变革：非职业学者借AI攻克难题，人类转向提炼与联结，形式化验证正成为AI证明的新信任基础。 综合评分： 82 文章分类： 其他

科技｜AI宣布森多夫猜想告破！陶哲轩发现它隐藏的更强结果

信息安全研究

2026年8月18日 15:00 北京

在小说阅读器读本章

去阅读

点击蓝字 关注我们

多项式是数学最基础的研究对象之一，根与导数临界点的关系，更是复分析里一个经典方向。森多夫猜想（Sendov’s conjecture）就是其中大名鼎鼎的难题。 1958年，保加利亚数学家布拉戈维斯特・森多夫提出该猜想。高斯‑卢卡斯定理早已告诉我们：多项式全部临界点落在根的凸包当中；而森多夫猜想则给出更强的局部约束——每一个根的附近，就藏着临界点。 过去几十年，数学家只能证明低次多项式成立，或是 “次数足够大时成立”，始终没能完成对全部次数的普适证明。陶哲轩也曾对该问题开展过相关研究。2026 年 8 月，研究者Lech Mazur公布一套结合计算机辅助与 AI 形式化手段的完整证明，宣称猜想对所有大于等于2的多项式次数全部成立，陶哲轩也对证明做了简化重形式化工作。不过这份证明还在等待同行完整核验，尚未形成学界公认的定论。 这个猜想里半径1是最优边界，不能再缩小，(z^n-1) 就是经典的极值案例。看似简单的几何命题，却足足考验了一代代数学家近70年。 随着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 能证明定理了，但远未结束。被解决的问题打开的往往是更多的问题。

（来源：机器之心）

免责声明：

本文所载程序、技术方法仅面向合法合规的安全研究与教学场景，旨在提升网络安全防护能力，具有明确的技术研究属性。

任何单位或个人未经授权，将本文内容用于攻击、破坏等非法用途的，由此引发的全部法律责任、民事赔偿及连带责任，均由行为人独立承担，本站不承担任何连带责任。

本站内容均为技术交流与知识分享目的发布，若存在版权侵权或其他异议，请通过邮件联系处理，具体联系方式可点击页面上方的联系我。

本文转载自：信息安全研究 《科技｜AI宣布森多夫猜想告破！陶哲轩发现它隐藏的更强结果》