AI-Assisted Proof of Sendov's Conjecture Also Settles Phelps-Rodriguez Conjecture
Lech Mazur, a startup CEO, announced a computer-assisted proof of Sendov's conjecture for all degrees n≥2, completed with GPT-5.6 Pro and about 90,000 lines of Lean 4 code. Terence Tao digested and simplified the proof, reducing the Lean code to about 15,000 lines, and found that the argument also proves the stronger Phelps-Rodriguez conjecture from 1972, marking a landmark AI-assisted result in complex analysis.
Coverage timeline
机器之心机器之心
编辑｜冷猫 随着 AI 推理能力迎来井喷式的发展，数学研究正在经历一场深刻变化。那些曾经困扰人类数十年的未解难题，正在 AI 的辅助下加速解决。 这不，又有一个至今约 70 年的数学猜想：森多夫猜想，被一位名叫 Lech Mazur 的初创科技公司 CEO，借助 AI 完成了证明。 证明论文题为「A Computer-Assisted Proof of Sendov's Conjecture」，作者 Lech Mazur 宣布：森多夫猜想对所有次数 n≥2 成立， 证明在 GPT-5.6 Pro 辅助下完成 ，配有约 9 万行 Lean 4 形式化代码。 论文链接：https://www.proofatlas.ai/papers/sendov-conjecture/SENDOV_CONJECTURE_PROOF_AUGUST_5_2026.pdf 8 月 12 日，陶哲轩在博客发文，称自己花了数天时间（同样在大量 AI 辅助下）将这份证明消化、简化并重新形式化，新版 Lean 代码缩减到约 1.5 万行。 博客链接：https://terrytao.wordpress.com/2026/08/12/a-digestion-of-the-proof-of-sendovs-conjecture/ 更关键的是，他发现整理后的论证实际上证明了一个更强的命题，1972 年提出的 Phelps-Rodriguez 猜想也随之被解决。 这意味着，复分析领域最著名的公开问题之一，在 AI 的参与下一次性画上了句号。 森多夫猜想：一个优雅到令人沮丧的问题 森多夫猜想由保加利亚数学家 Blagovest Sendov 于 1958 年前后提出，陈述极其简洁： 设 p (z) 是一个 n 次复多项式（n≥2），其所有零点都在闭单位圆盘内（即 |z|≤1）。那么，对 p 的任意零点 a，至少存在一个临界点 w（即导数 p'(z) 的零点），使得 |w - a| ≤ 1。 换一种说法：如果一个复系数多项式的所有根都位于单位圆内，那么每一个根附近，是否一定存在一个距离不超过 1 的临界点？ 示意图由 AI 生成 这个猜想的背景来自经典的高斯 - 卢卡斯定理（Gauss-Lucas theorem）。该定理说：多项式的所有临界点都落在其零点构成的凸包内部。这是一个整体性结
