投稿者: 2026 年 1 月 14 日、OpenAI の大規模言語モデル「GPT-5.2 Pro」と Harmonic 社の形式証明支援 AI「Aristotle」が協働し、長年未解決であった数学の難問「エルデシュ問題 #728」を解決したことが報じられました。
エルデシュ問題とは、20 世紀を代表する数学者の一人であるポール・エルデシュが提起した、数多くの未解決問題の総称です。彼は生涯で 1500 本以上の論文を共著で発表したことで知られ、様々な数学の分野に膨大な問題を遺しました。これらの問題は、簡潔な問いかけでありながら証明が非常に難しいものが多く、解決者にはエルデシュ自身から懸賞金が贈られることもありました。
今回の成果が特に注目されるのは、AI が既存の文献にはない全く新しい証明を主体的に生成した点です。これは、AI が人間よりも先に実質的な解決策に到達した初のエルデシュ問題として、画期的な出来事とされています。過去に AI が数学の問題を解いた事例は、既存の証明を探索・検証するものが主でしたが、今回は AI の数学的能力が新たな段階へ進んだことを示しています。
エルデシュ問題 #728 は、1975 年に提起された、階乗の可除性に関する数論の難問です。解決プロセスにおいて、GPT-5.2 Pro は問題の意図を整理し、自ら補題を立てて証明案を作成しました。途中で行き詰まると「ここはまだ解決できていない」と自己申告するなど、高度な自律性も示したと報告されています。最終的な証明は、Aristotle が形式検証言語 Lean を用いて検証し、完成しました。
著名な数学者テレンス・タオ氏も、この成果を「ほぼ自律的に AI がエルデシュ問題を解いた最初の事例」と高く評価しています。しかし、まだ「AI だけでフィールズ賞級の大問題を解いた」という段階ではありません。専門家によれば、今回解決された問題の難易度は“中堅クラス”であり、解決の過程では人間の研究者による解釈の調整や最終確認といった補助が必要だったとされています。
この技術は #728 以外にも、エルデシュ問題 #124 や #729 など複数の問題で進展をもたらしており、AI による数学研究への貢献は広がりつつあります。今回の出来事は、AI が単なる計算ツールではなく、新たな数学的発見のパートナーとなり得る可能性を示しており、今後の研究スタイルに大きな影響を与える象徴的な一歩と言えるでしょう。