对Sendov猜想证明的消化: AI生成证明经Lean验证后整理并完全解决相关猜想

摘要

帖子讨论Sendov猜想、其Phelps–Rodriguez加强版以及内点版本Conjecture 3。此前这些猜想在部分情形和充分大情形已有结果，中间情形未决。最近Lech Mazur用AI工具解决Sendov猜想，证明经Lean验证，但AI生成的证明尚未整理成可发表预印本。作者花数日、借助大量AI辅助进行消化，将其置于既有文献语境并简化以突出核心思路；聊天记录仅占整理工作的一部分，其余用纸笔或更多AI代理完成。相同论证还给出Rubinstein定理的新证明，并表明Conjecture 3成立，从而完全解决Sendov猜想与Phelps–Rodriguez猜想；证明相当初等，未使用复分析。