森道夫猜想获完整证明与形式化验证

近日，复分析领域的经典难题Sendov猜想与Phelps-Rodriguez猜想获完全解决。该猜想核心探讨单位圆盘内多项式零点与其临界点的几何距离关系。本次突破由数学家Lech Mazur借助人工智能工具生成初始证明，并经过领域专家进行严谨的逻辑重构与人工消化。团队随后利用Lean定理证明器完成全量形式化验证，代码量精简至约一万五千行。值得注意的是，该证明过程巧妙规避了传统的复分析工具，仅凭代数基本定理与基础均值不等式即可推演，展现出高度的初等性。这一成果不仅彻底终结了困扰学界多年的猜想之争，更首次以完整案例确立了人工智能辅助数学证明的人机协同标准流程。目前，该研究路径已为多项式临界点理论提供新视角，而相关扩展猜想如Borcea猜想与Smale问题仍待进一步探索。