AI証明を整理しSendov予想を解決

数学界の長年未解決問題「Sendov予想」が、AI支援による解析と形式検証技術の活用により完全証明された。この予想は、単位円板内に零点を持つ多項式の各零点に対し、導関数の零点が一定距離内に存在することを主張するもので、その強化版である「Phelps-Rodriguez予想」も同時に解決された。 証明のプロセスは、AI支援数学研究の新基準を確立している。元となる証明はLech Mazur氏がAIツールを用いて生成したものであったが、学界で発表可能な形式への変換には専門家の介入が必要だった。本研究チームはAIの支援を受けつつ、複素解析を排除し、代数学と基本不等式のみで構成される初等的な論理へ再構築した。さらに、形式検証環境「Lean」を用いて全論理を1万5000行というコンパクトなコードで再実装し、元の約9万行から大幅に簡素化に成功した。 本成果により両予想は一般ケースで成立することが確定した。同時にRubinstein定理の新たな証明も導出された。AIを活用した数学的発見のワークフローが、人間の直感と計算機支援の融合により、純数学の難問解決において実証された点に注目が集まっている。 関連するBorcea予想やSchmeisser予想、Smale問題などは依然として未解決であり、本アプローチの拡張性には限界があることが示唆される。今後はAI支援数学解析の適用範囲拡大と、形式的検証システムの自動化・大規模化が今後の技術的課題となる。