一个只有一句话、却悬置了 68 年的数学猜想，被 AI 生成的证明终结了。菲尔兹奖得主陶哲轩随后花数天时间、借助 AI 辅助，把机器那份约 9 万行的 Lean 形式化证明，消化成任何人都能读懂的简洁证明——并发现机器其实顺手证明了更强的结论。
一句话的猜想，68 年没解
森多夫猜想（1958 年，保加利亚数学家 Blagovest Sendov 提出）陈述简单到不像开放问题：任意 n 次多项式，若所有根都在单位圆盘内，则对每个根 a，都存在一个临界点（导数的零点），与 a 的距离不超过 1。
高斯–卢卡斯定理保证临界点位于根的凸包内，但「每个根附近 1 以内都有临界点」要强得多。几十年来，小次数情形（Rubinstein，以及后来 Brown–Xiang 等）和大次数情形（陶哲轩 2020 年）陆续被解决，中间地带一直悬着。
AI 做了什么
8 月 5 日，Lech Mazur 用 AI 定理证明工具 ProofAtlas 给出覆盖所有次数的证明，并经 Lean 证明助手端到端形式化验证。问题在于：机器证明约 9 万行，人没法读，也不能直接发表。
于是有了「消化」这一步。陶哲轩借助 AI（包括 ChatGPT 会话）花了数天重构论证：对接已有文献、删掉冗余、提炼主线。结果出奇地初等——除了代数基本定理，用到的最深不等式只是 Maclaurin 不等式的一个特例（由均值不等式加归纳即可推出）。
消化过程带来两个意外：其一，论证实际上证明的是「内部版本」，同时推出森多夫猜想和更强的 Phelps–Rodriguez 猜想；其二，陶哲轩用 AI agent 把整个证明重新形式化，只用了约 1.5 万行，比机器原版精简 6 倍。
为什么机器赢了
证明依赖的四条「沟通恒等式」（质心、极、两个原点恒等式）全都藏在机器论证的碎片里。机器靠搜索把它们翻出来；人类 68 年没这么组合，是因为优雅的既有成果形成了引力场。机器没有这个包袱——它不需要证明好看，只需要证明存在。
产业含义
这是陶哲轩反复描述的流水线最完整的一次演示：生成 → 验证 → 阐述 → 发表 → 经典化。AI 负责生成和验证（Lean 把关），人类负责阐述和经典化——把「验证过但读不懂」变成「能教、能传播、能写进教科书」的知识。瓶颈已经转移：找到证明正在变得廉价，消化证明才是稀缺能力。
对 AI 产业而言，信号大于一条定理本身：AI 工具解决了一个纯数学开放问题，而当代最强的数学家把机器输出当作合作者用了好几天。这个模式与编程 agent 的路径一致：广泛生成、严格验证、精心策展。面向实验室的 AI 科研智能体（如 Polaris）已经在把「生成–验证–消化」工作流工业化。
行动建议
- 押注验证，而不只是生成。Lean 这类工具把不可靠的模型变成可用工具。
- 把 AI 输出当原材料。9 万行不可用，陶哲轩的 1.5 万行才是真正的成果。
- 公开消化。陶哲轩的博客与聊天记录是「把机器发现变成社区知识」的模板。
- 关注流水线。掌握「生成–验证–消化」的团队将产出研究级成果，而不只是草稿。
