8月中旬，一条数学新闻刷屏了：悬了将近70年的森多夫猜想（Sendov’s Conjecture）被"攻破"了。证明者不是职业数学家，而是一家初创公司的CEO Lech Mazur，按论文自述，证明在GPT-5.6 Pro辅助下完成，配有约9万行Lean 4形式化代码。机器之心
但对关注形式化证明的人来说，这条新闻里真正值得看的不是"攻破"本身，而是之后发生的事：8月12日，陶哲轩在博客发文，称自己花了数天（同样在大量AI辅助下）将这份证明消化、简化并重新形式化，新版Lean代码从9万行缩减到约1.5万行，并已在GitHub开源。机器之心更关键的是，整理后的论证实际上证明了一个更强的命题，1972年提出的Phelps-Rodriguez猜想也随之被解决。微博一石二鸟。
先给不熟悉背景的人一个30秒科普。森多夫猜想的陈述极其简洁：设p(z)是一个n次（n≥2）复多项式，所有零点都在闭单位圆盘内，那么对它的任意零点a，距离1以内必定存在至少一个临界点（导数的零点）。一个直观的图像：把零点想象成平面上的电荷，临界点就是这些电荷产生的平衡点。经典的高斯-卢卡斯定理只说平衡点不会跑出电荷构成的凸包，森多夫猜想则进一步问：每个电荷的"一步之内"是否一定有平衡点？常数1不可改进——z^n−1恰好就是等号成立的情形。就是这种"谁都能看懂陈述、几十年没人证出来"的问题，卡了将近70年。
那么陶哲轩的"消化"到底做了什么？这是整个事件里信息密度最高的部分。
按他博客的梳理，证明的骨架其实不复杂：整体走反证法，假设存在反例。先归一化，把零点a旋转到[0,1)上的实数，再把临界点改写为倒数坐标q_j=1/(a−w_j)，“距离1以内没有临界点"就变成了所有q_j都在单位圆盘内。接着从多项式及其导数在几个自然位置求值，得到四条"通讯恒等式”——质心恒等式、极化恒等式、第一和第二原点恒等式。关键的转折在于：从这里开始，多项式p本身不再出场，矛盾完全由"两组点都在圆盘内+四条恒等式"推出。论证随后分叉：低次数n≤5直接用积分估计收尾；n≥101解析地证明两个核心不等式不可能同时成立；最麻烦的5≤n≤100区间，用精确有理数的Bernstein多项式证书做数值验证，全程由Lean检验；边界情形|a|=1改用Meir-Sharma恒等式，精确刻画了等号成立的条件——而这正是Phelps-Rodriguez猜想中需要排除的极端族，更强的结论因此作为推论直接得出。
陶哲轩对这份证明的评价相当高：“令人惊讶地初等”，除了代数基本定理和Möbius变换的基本性质外没有用到任何复分析工具，最深的不等式输入只是Maclaurin不等式的一个特殊情形。
注意这里有两个数字，信息量很大：从9万行到1.5万行。这不是"代码整理"。AI生成的形式化里，大量行数是搜索和试错留下的冗余脚手架，消化做的事是重构论证、找出它真正的结构——而更强结论的发现恰恰来自这次重构。换句话说，消化不是排版，是再发现。这也回答了很多人看完新闻后的疑问：机器都验证过了，人类还干什么？机器能保证"每一步推导都正确"，但它不会告诉你"这个证明到底在证明什么"。
把这件事放进更长的时间线里看，它其实是陶哲轩7月底在ICM 2026大会上公开预警的那个图景的第一个完整样本。那场题为《Mathematics in the age of AI》的演讲，他先甩了一组数据：独立评测First Proof今年5月28日的第二批测试，10道全新研究级数学题，四套AI系统在受控条件下解出了7道"可发表质量"的答案，单题算力成本10到1000美元。量子位
然后他提出了"证明消化不良"的概念：数学的流水线是生成→验证→表述→发表→正典化，AI把第一环节的速度拉爆了，验证有Lean兜底，但后面的表述、消化、正典化全靠人的志愿劳动，各环节流速对不上，整个系统就会失配。量子位
演讲里他还展示了一张私藏照片：1991年Bourgain的一篇论文，页边写满年轻陶哲轩的手写批注，其中一句是"我恨Jean Bourgain"。看不懂、被卡住、边骂边啃，这个过程本身就是数学传承的一部分，人类表述里的瑕疵反而对读者有益。量子位而AI生成的证明，读者连"被卡住"的机会都没有。
他的判断是，数学将从"证明稀缺"的时代进入"证明过剩"的时代。量子位症状已经出现了：仅在收录Erdős遗留问题的网站上，就躺着几十份AI生成的证明提交，很多大概率是对的，但没有一位人类专家自愿站出来核验背书，有些提交者自己承认"我没这个资格验"。
对照之下再看森多夫猜想，它的可信度就清楚在哪里了：它有一条完整的信任链——约9万行的完整Lean 4形式化（每一步都过机器类型检查），加上陶哲轩消化、简化、再形式化为1.5万行并开源。机器之心而几乎同一时间，Crouzeix猜想也被宣称"由AI解决"，知乎相关讨论里，本身就在该研究方向上的Teng Zhang直言不讳地质疑作者不懂矩阵分析。知乎两个事件放在一起，给出的教训很一致：看AI证明，别只看发布会，要看验证链。
社区的反应同样值得品味。知乎问题下那条2054赞、192条评论的高赞回答，来自Teng Zhang本人——他是Tang-Zhang猜想里的Zhang，森多夫猜想正是他博士期间的课题。回答的开头，他说这个陪了自己整个博士阶段的猜想被AI解决了，自己的青春结束了。知乎评论区很复杂：有人安慰"收拾心情，重新出发"，有人讨论证明攻坚一旦工业化，一部分数学进展会变成资金和算力的问题，还有人说"学术论文的前瞻性会低于明星研究者的博客"。
学术归属之争也已经开始了：Teng Zhang在回答中指出，用Meir-Sharma恒等式给出Rubinstein定理的简洁证明并非新东西，他和Tang早先解决de Bruin–Sharma问题的论文里就已注意到。知乎而陶哲轩在ICM演讲中引用《莱顿宣言》时强调的方向正是：降低"第一个解出"的权重，提高"消化"的权重。量子位
最后，给不同需求的读者一些实在的建议。
如果你有Lean 4 / mathlib基础：这可能是历史上参与门槛最低的一次"严肃数学成果审计"。陶哲轩的1.5万行版本已开源在GitHub（入口在他的博客），依赖树可以一路追到mathlib，值得花时间读一读；也值得盯着社区能不能复核完毕，或者找出形式化保真度上的问题——即形式化陈述是否与原猜想的表述严格对应，这一点机器验证并不兜底。
如果你只想围观：盯住四个信号。一是论文目前挂在Mazur自己的ProofAtlas平台上，属于预印本，专业同行评审和期刊接收怎么推进；二是1.5万行Lean版本的社区审计进展；三是陶哲轩在博客末尾列出的仍开放的相关猜想——Borcea猜想、Schmeisser猜想和Smale问题，他坦言自己也尝试用AI攻击过但"没有取得显著成功"，这几个很可能是下一批被围攻的目标。机器之心四是据Teng Zhang透露，陶哲轩已经用AI解决了Tang-Zhang猜想中n充分大的情形——多米诺骨牌才刚倒下第一张。
陶哲轩在ICM演讲里给过一条规则，我觉得它该被贴在AI证定理时代的门口：“如果作者不能令人信服地证明，自己可以就其成果做一场清晰的、专家水平的、正确且归属得当的报告，那么这个成果就不应该发表。”
森多夫猜想大概率是被解决了。但这件事真正的启示是：会证明的能力在贬值，会消化的能力在升值。而形式化证明的位置，也在随之悄悄变化——从数学家自查证明的小众工具，变成AI时代数学的信任基础设施。这个变化，值得长期盯下去。
