AI辅助破解70年数学悬案：森多夫猜想被证明

随着人工智能推理能力的快速进化，数学研究领域正迎来一场深刻的范式变革。数十年来悬而未决的经典难题，如今正借助AI工具加速获得突破。

近期，一项跨越近70年的数学猜想——森多夫猜想，由非学术背景的创业者借助AI工具完成了完整证明。该证明在大语言模型辅助下完成，配套的形式化代码规模庞大，最终确认森多夫猜想对所有次数n≥2的情况均成立。

后续知名数学家对该证明进行了重构与简化，不仅精简了代码量，更意外发现原证明可以推导出一个更强的命题，顺带解决了另一项搁置数十年的数学猜想。这意味着复分析领域的这一知名公开难题，在AI的参与下得到了彻底解决。

森多夫猜想：一个优雅到令人沮丧的问题

森多夫猜想由保加利亚数学家在1958年左右提出，其表述极为简洁清晰：假设p(z)是一个n次复多项式（n≥2），且所有零点都位于闭单位圆盘内（即|z|≤1），那么对于p的任意零点a，至少存在一个临界点w（也就是导数p’(z)的零点），使得|w - a| ≤1。

用更直白的话来说：如果一个复系数多项式的所有根都落在单位圆内部，那么每一个根的周围，必然存在一个距离不超过1的临界点。

这一猜想的提出基于经典的高斯-卢卡斯定理，该定理指出多项式的所有临界点都位于其零点构成的凸包内部，属于整体性的结论。而森多夫猜想则聚焦于局部特性，可以用直观的物理图像理解：将多项式的零点比作平面上的电荷，临界点则相当于这些电荷产生的平衡点。高斯-卢卡斯定理保证平衡点不会超出电荷围成的区域，而森多夫猜想则进一步指出，每个电荷的“一步范围”内必然存在平衡点。

值得注意的是，猜想中的常数1是无法被优化的。以多项式p(z)=z^n -1为例，其零点为n个单位根，唯一的临界点是原点的n-1重根，每个零点到最近临界点的距离恰好为1。这一特例也正是后续更强猜想需要排除特定情况的原因。

尽管森多夫猜想的表述极为简洁，但它的证明进度却异常缓慢：

• 1969年，Meir和Sharma证明了n<6的情况
• 1991年，Brown将证明推进到n<7
• 1996年，Borcea进一步将范围扩大到n<8
• 1999年，Brown和Xiang将结果推进到n<9，此后的20多年间，低次数的证明再无新的进展
• 2020年，知名数学家证明了当n足够大时森多夫猜想成立，但论证使用了解析延拓等定性工具，无法给出明确的次数阈值
• 2026年初，华人数学家将前述阈值进行了显式化处理，确定为10^200000

本次完成证明的创作者并非职业学术数学家，他是一家初创科技公司的创始人兼CEO，同时也是专注于AI优先形式化数学的平台创建者。该平台将可视化解释、形式化陈述、完整源码、依赖关系和反驳路径整合在一张持续更新的证据图谱中。

根据论文描述，AI参与了本次证明的数学探索、证明开发、测试与审查全流程，最终产出的形式化代码约有9万行。

证明思路与更强猜想的解决

知名数学家对原证明进行了完整的重构与简化，他指出，经过消化后的论证实际上证明了更强的命题，从而一举解决了森多夫猜想和另一项1972年提出的猜想。整个证明采用反证法框架：

核心设定

假设存在反例，即存在一个n次多项式p，其所有零点都在闭单位圆盘内，但存在某个零点a，其周围1单位距离内没有任何临界点。

归一化处理

通过旋转变换，将零点a转换为[0,1)区间内的实数，再将临界点转换为倒数坐标。此时“距离1以内没有临界点”的条件可以被简化，反例被转化为单位圆盘内的两组点：其余零点和倒数临界点。

建立核心恒等式

研究者将核心的四条关系称为“通讯恒等式”，包括质心恒等式、极化恒等式、第一原点恒等式和第二原点恒等式。这些恒等式通过在几个自然位置对多项式及其导数求值得到。一个意外的转折是，后续的论证中多项式本身不再出现，矛盾完全从两组点的位置约束和这四条恒等式推导而来。

分支点分析

结合极化恒等式与相关变换的估计，可以推导出一个关键的积分下界，这也是整个论证中唯一用到a为实数的步骤，同时也是后续论证分叉的起点。

对于低次数情况（n≤5）：通过标量控制被积函数的每一项，可以证明得到的积分与之前推导的积分下界直接矛盾，从而完成低次数情况的证明。

对于高次数情况（n≥5）：需要同时建立两个不等式。这两个不等式对于核心参数划定的可行域互不相容：当n≥101时，可以通过解析方法证明两个不等式无法同时成立；而5≤n≤100的区间则通过精确数值验证，整个过程由形式化工具进行检验。

对于边界情况（|a|=1）：虽然该情况已经提前解决，但研究者使用同一套框架给出了新的证明，精准刻画了等号成立的条件，这恰好就是另一项更强猜想需要排除的极端情况。

研究者评价本次的证明“令人惊讶地初等”，除了代数基本定理和基础变换的性质外，没有用到任何复杂的复分析工具，用到的最深的不等式也只是基础的算术平均相关结论。

另一项被一并解决的猜想是1972年提出的Phelps-Rodriguez猜想，它在森多夫猜想的基础上要求临界点与零点的距离严格小于1，除非a位于单位圆周上且多项式为特定形式。由于本次证明精准刻画了等号成立的条件，因此该猜想作为推论也被直接解决。

研究者将重构后的论证形式化为约1.5万行的形式化代码，目前已在开源平台公开。

AI正在重塑数学研究的范式

本次森多夫猜想的证明，也让人们重新审视AI在数学研究中的角色：

首先，证明者的身份边界被打破。非职业学术背景的创作者借助AI工具完成了困扰专业学者数十年的难题，这打破了传统上只有职业数学家才能攻克顶级数学难题的固有认知。

其次，人机协作的新模式正在形成。整个证明流程呈现出清晰的分工：AI负责生成证明和形式化验证，人类数学家负责判断、提炼和联结不同的论证环节，双方的优势得到充分结合。

最后，形式化验证为AI生成的证明提供了可靠的信任基础。在传统研究中，证明的可信度依赖同行评审，而形式化工具可以确保每一步逻辑都是严格无误的，这对于AI生成的内容尤为重要。

研究者在公开分析中也列出了目前仍然未解决的相关猜想，并坦言自己尝试使用AI工具攻击这些问题，但并未取得显著进展。这也说明，AI虽然已经能够协助完成复杂的数学证明，但距离完全自主攻克数学难题还有很长的路要走。每一个被解决的经典难题，往往都会打开更多新的研究方向与问题。