AI 攻克 Sendov 猜想，Terry Tao 详解证明
A digestion of the proof of Sendov's conjecture
困扰数学界多年的 Sendov 猜想及其加强版 Phelps–Rodriguez 猜想，近日由 Lech Mazur 借助 AI 工具成功证明，并在 Lean 中完成形式化验证。作为该领域的资深研究者，我花费数日时间，在 AI 的辅助下对这份机器生成的证明进行了深度“消化”。我将原本晦涩复杂的论证过程转化为人类可读的预印本，梳理了其与过往文献的关联，并大幅简化了核心逻辑。令人惊讶的是，最终证明竟异常基础，仅依赖代数基本定理和 Maclaurin 不等式，无需复杂的复分析技巧。这项工作不仅解决了中间阶数多项式的遗留问题，还以更精简的代码量（约 1.5 万行）重新形式化了整个论证。
这个证明最终变得异常基础，除了代数基本定理和关于 Möbius 变换的基本事实外，没有使用任何复分析；而作为输入的最深不等式仅仅是 Maclaurin 不等式。
HN 评论区
36- fwlr
AI 的进展对一些数学家的心理冲击肯定相当残酷。对我来说，这大大打破了数学的神秘感。
你依然需要大量技能去消化和理解这些证明，但“这就是最坏的情况了”。我想象，很大一部分数学家的动力在于成为“第一个”或者攻克别人攻不下的难题。如果数学变成了与 AI 协作获取 Lean 证书，然后本质上将其逆向工程成可消化的内容，那这就从根本上变成了一种不同的追求。
软件工程受到的影响似乎小一些？不过，如果你认同自己热爱编码，那或许也类似？我一直喜欢写代码能带来的成果，也享受过去 ~30 年手工编码的工艺。但自从 Opus 4.6 之后，我一次也没怀念过手工写代码，我再也回不去了。
- glimshe
当 HN 上这么多人抱怨 AI 时，一位该领域的绝对大师却在毫无自我怀疑或负面情绪地使用它。只是更高效、更快速地完成任务，同时依然保持在顶尖位置。
- brotchie
让事物变得可理解，与生成初始产物一样，都是智能的一部分。即使证明在 Lean 中通过检查（或者代码运行并通过 QA），如果它一团糟，就很难用它来做进一步的工作。
这不仅关乎前沿数学。关于“消化版”与“原版”的这一点，在座的某些人应该会觉得熟悉：
> 这个形式化版本比原版更精简（代码约 15,000 行，而原版证明约为 90,000 行）。
如果你曾试图将一段过度依赖直觉（vibed）的代码变成有意义的东西：
> 我花了好几天（在 AI 的大力协助下）才完成这种消化工作，将证明置于与先前文献的恰当语境中，并简化、精简论证以突出核心思想。
如果你看到某些东西令人困惑或过于花哨，请不要假设它一定有某种你不懂的好理由然后就此作罢——多问问题，让它简化，试着把它弄明白。未来的你会感激现在的你。