AIがグラフ理論の20年来の予想を解決
研究者らは、セミストリーミングマッチングにおいて貪欲アルゴリズムが最適近似比を達成することを証明し、Lean証明アシスタントを用いて形式検証しました。これは長年の予想を解決し、数学的発見におけるAIの役割を示しています。
コンピュータ科学と数学の交差点で、20年にわたるグラフ理論の予想がAI支援による証明で解決されました。研究者たちは、セミストリーミング（semi-streaming）マッチング問題において、貪欲アルゴリズムが最適な近似比を達成することを厳密に証明しました。
この成果は、Sepehr Assadi、@mangooqwq、および別の共同研究者によって達成されました。彼らは10行という簡潔なアルゴリズムを示しただけでなく、Lean証明アシスタントを使って形式検証を行い、推論の厳密性を保証しました。セミストリーミングマッチングは大規模グラフデータを扱うための重要な技術であり、この結果は貪欲戦略が実際に最適な選択であることを意味します。
Leanは対話型定理証明器であり、数学者がコンピュータでチェック可能な形で証明を記述することを可能にします。今回の成功は、長年未解決だった難問をAIが支援できることを示し、将来の数学的発見に新たな道を開くものです。関連論文はarXivで公開され、コードと証明も公開されています。