【チャッピー快挙】GPT5.4が素人のプロンプトで60年来の数学難問エルデシュ問題を証明

　2026年4月、数学の高度な専門教育を受けていない23歳のLiam Price氏が、GPT-5.4 Proとの対話を通じて、ポール・エルデシュが提唱した未解決問題「Erdos Problem #1196」を証明した。この問題は原始集合と呼ばれる、どの要素も他の要素を割り切らない整数の集合の密度に関する予想であり、約60年にわたって専門家による証明がなされていなかった。Price氏は厳密な定式化から始める従来の手法ではなく、直感的にAIへ質問を投げてアイデアを生成させるアプローチをとった。

　約80分の対話の中で、GPT-5.4 Proはフォン・マンゴルト関数とマルコフ連鎖を組み合わせた証明手法を提示した。この数学的ツール自体は既知のものだったが、同問題の解決に適用した例はこれまでになかった。この結果を受け、フィールズ賞受賞者のテレンス・タオ氏はAIが導き出した証明を確認し、過去の数学者による研究アプローチが初期段階で方向性を誤っていたと指摘した。2026年5月には、タオ氏やPrice氏を含む8名の共同著者によって、プレプリントサーバーのarXivに論文が公開された。


　この論文では1196番の証明に加えて、関連する1217番の問題やバンクス・マーティン予想に関する成果もまとめられている。さらに、AIスタートアップ企業のMath, Inc.は、定理証明支援言語であるLeanを用いてこの証明の形式的な検証を実施した。検証プロセスにおいて同社のAIモデルは数時間で約7200行のLeanコードを生成し、その後のコード最適化によって約4000行まで圧縮された。

　これにより、AIが提示した証明の論理的な正確性が機械的にも裏付けられた。大規模言語モデルが専門家の見落としていたアプローチを発見し、未解決問題の解決に直接寄与した事例として、複数の学術メディアやテクノロジー報道機関が事実関係を報じている。