31年間解けなかった数学の難問、マイクロソフト研究者とAIの協力で証明

米マイクロソフトの研究機関であるマイクロソフト・リサーチなどの研究チームは、高次元幾何学分野において31年間にわたり未解決だった数学の難問「KLS予想（Kannan–Lovász–Simonovits conjecture）」を証明したと発表した。研究者が方向性を指示し、AIエージェントが数理的な可能性を探索する人間とAIの協調プロセスによって達成された。

KLS予想は1995年に提唱された問題で、広範な高次元確率分布において、最も優れた平坦な切断（超平面）があらゆる形状の最良の切断と定数倍の範囲内で同等に有効であるかという幾何学的な原理を問うものだ。この性質は高次元空間内をランダムに探索するサンプリングの効率を左右するため、統計学や最適化、計算機科学で用いられるランダム化アルゴリズムの基礎理論として重視されてきた。これまで多くの証拠が積み重ねられてきたものの、完全な証明には至っていなかった。

研究チームは、次元数の増加に伴って境界値が緩やかに増大することを許容していた2026年7月の先行成果を足がかりに研究を開始した。AIエージェントと連携しながら、高階テンソル計算を伴う100通り以上の候補アプローチを探索し、証明の基盤となる新たな数学的基準を導き出した。さらに、過去の線形計画法アルゴリズム研究から着想を得て、この基準を再帰的に繰り返し適用する手法を構築した。各段階で生じる微小な誤差の累積が次元数に依存しない普遍定数に収まることを示し、2026年10月4日付けの論文で完全な証明をまとめた。

今回の成果は、最先端モデルに単独で難問を解かせる手法ではなく、人間主導の探索が鍵となった。AIエージェントが複数のアイデアを並行して展開し、研究者が中間結果を確認して有望でない方向を枝刈りした。同等の計算量を用いて誘導なしでAI単体に解かせようとした別検証の試みは失敗に終わっており、AIの探索能力と人間の数学的判断の双方が不可欠だったと説明している。

証明が公開された同日には、別の専門家グループが第一版の手法を発展させた独自の完全証明を並行して発表したほか、さらなる別証明や証明支援システム「Lean 4」を用いた機械検証（形式検証）も相次いで公開された。研究チームは現在、証明の記述を短縮した版の作成とLeanによる検証の拡張を進めており、最終確認を経て公開する予定としている。