AI 助证森多夫猜想，陶哲轩简化并证出更强命题
AI 辅助完成著名数学猜想证明，经陶哲轩验证并简化，还顺带解决一个更强猜想，展现 AI 在数学研究中的真实作用。
森多夫猜想（关于复多项式每个零点附近必有临界点的几何命题）由一位 CEO 借助 AI 完成证明，并用约 9 万行 Lean 代码验证。陶哲轩消化后把证明简化到 1.5 万行，还发现它其实解决了更强的 Phelps-Rodriguez 猜想。
正文摘录
.jpg) 编辑｜冷猫 随着 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/SENDOVCONJECTUREPROOFAUGUST52026.pdf 8 月 12 日，陶哲轩在博客发文，称自己花了数天时间（同样在大量 AI 辅助下）将这份证明消化、简化并重新形式化，新版 Lean 代码缩减到约 1.5 万行。