RecodeX 重构消息，初创公司CEO Lech Mazur借助AI完成了森多夫猜想的证明，论文宣称对所有次数n≥2成立，并配有约9万行Lean 4形式化代码。8月12日，陶哲轩在博客发文称，经数天消化与重新形式化，他将Lean代码缩减至约1.5万行，并发现该论证实际证明了更强的1972年Phelps-Rodriguez猜想。这意味着复分析领域两大经典猜想均被解决。陶哲轩已将重新形式化的代码开源至GitHub。