AI 攻克 Sendov 猜想，Terry Tao 详解证明

A digestion of the proof of Sendov's conjecture

困扰数学界多年的 Sendov 猜想及其加强版 Phelps–Rodriguez 猜想，近日由 Lech Mazur 借助 AI 工具成功证明，并在 Lean 中完成形式化验证。作为该领域的资深研究者，我花费数日时间，在 AI 的辅助下对这份机器生成的证明进行了深度“消化”。我将原本晦涩复杂的论证过程转化为人类可读的预印本，梳理了其与过往文献的关联，并大幅简化了核心逻辑。令人惊讶的是，最终证明竟异常基础，仅依赖代数基本定理和 Maclaurin 不等式，无需复杂的复分析技巧。这项工作不仅解决了中间阶数多项式的遗留问题，还以更精简的代码量（约 1.5 万行）重新形式化了整个论证。