AI支援で７０年未解決の森多夫予想に証明
約７０年間未解決だった数学問題「森多夫予想」が、AI支援による形式的証明で解決されたと発表されました。スタートアップ企業CEOのLech Mazur氏が発表した論文「A Computer Assisted Proof of Sendov's Conjecture」では、次数nが２以上のすべての場合で予想が成立すると示されています。今回の証明では、GPT 5.6 Proの支援を活用し、約９万行に及ぶLean 4形式化コードを作成しました。AIの推論能力向上により、従来は数十年単位で解決が難しかった数学研究が加速しており、今回の成果はAIと人間研究者の協力による新たな研究手法の可能性を示しています。