AIで数学の未解決問題をほぼ自動的に解くことに成功、AIツールにおける重要な進展に

20世紀で最も多くの論文を書いた数学者として知られるポール・エルデシュはその生涯で多くの未解決問題を発案しており、これらは「エルデシュの問題」として知られています。そのエルデシュの問題のうちの1問をGPT-5.2 Proが解決し、著名な数学者であるテレンス・タオ氏が「私たちの知る限り、既存の文献では再現されない、ほぼ自律的な解決であり、AIの能力が本当に向上したことを示すものだ」とコメントしています。

How We Used GPT-5.2 to Solve an Erdos Problem : r/singularity
https://www.reddit.com/r/singularity/comments/1q6vaxj/how_we_used_gpt52_to_solve_an_erdos_problem/

AI contributions to Erdős problems · teorth/erdosproblems Wiki · GitHub
https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems

Erdős Problem #728
https://www.erdosproblems.com/728

今回話題になっているエルデシュの問題の728番は、1975年にエルデシュらによって提唱された階乗の整除性に関する数論の問題で、「十分小さい定数Cとεが存在する時、『a!b!がn!(a+b-n)!を割り切る』かつ『a+bがn+C*log nよりも大きい』を満たすような整数(a,b,c)は無限に存在するか」というものです。ただし、タオ氏によれば当初の問題文は表現が曖昧で、例えば定数Cが小さい定数として意図されたのか、大きい定数として意図されたのかが判然としなかったと述べています。

この問題の解決については、GPT-5.2 Pro ProとAristotleというAIツールが主導的な役割を果たしました。

RedditユーザーのThunderBeanage氏は、これまでさまざまなLLMを用いて数学の証明を試みてきました。しかし、ThunderBeanage氏によれば、従来のLLMにインターネット検索を許すと、問題が未解決だと気づいて「解けない」と判断してしまい、解法探索を止めてしまうことがあったとのこと。そのため、プロンプトでネット検索しないように指示したりネット遮断でその挙動を避けたりしたそうです。また。ネットを遮断しても、今度は幻覚や致命的な飛躍が頻発し、正しい証明にならないことが大きな障害だったとThunderBeanage氏は述べています。

しかし、2025年12月に登場したGPT-5.2 Proは、証明を作る途中で埋め切れない補題がある場合に、無理にでっち上げず「ここが未解決だ」と正直に言う傾向があり、全体の骨格はかなりの割合で正しかったとのこと。そこで、ThunderBeanage氏は最終的に「ネットありのGPT-5.2で問題の意図と方針を整理し、LaTeXで記述した短いプロンプトを作る」→「別インスタンスのGPT-5.2にネットを禁止した上でそのプロンプトを与えて証明を書かせる」→「別インスタンスに検算と修正をさせる」という方法を考案しました。

1月4日にはGPT-5.2 Proが制約つきの証明を出力。ただし、この時は問題の曖昧さが原因で、正しく解決したと見なされなかったため、「a,b≦(1-ε)n」というより厳しい条件を課した解釈で解決を図ることとなりました。

ChatGPT - Erdos factorial divisibility
https://chatgpt.com/s/t_695bdbf3047c8191af842d03db356b1a

これをAcerFurというユーザーがAristotleに渡し、Leanで形式化しました。しかし、その後、コミュニティ内で議論が勃発し、定数Cをどのように解釈するかで再び厳しい制約を課す必要がでてきたとのこと。

そこで、ThunderBeanage氏がGPT-5.2 Proへ「追加制約を満たす形に議論をアップグレードできるか」を改めて問うたところ、GPT-5.2 Proは可能だと回答。そこで出力された新たな証明が、Aristotleによって形式化されました。その際、証明には小さな誤りが混ざっていたものの、Aristotleが自動的にギャップを修復してLeanで検証済みの形に仕上げられたそうです。

Factorial Divisibility Beyond the Logarithmic Barrier /Erdos728Updated.pdf - Google ドライブ
https://drive.google.com/file/d/1xRw8_o2C8HwmxMDnBR5OJlxXaW7jlYbz/view

エルデシュの問題に取り組んでいるタオ氏は、今回の証明について「AIがエルデシュ問題をほぼ自律的に解き切った」と評価しています。特に、既存文献には見当たらない結論がAIによって導かれたこと、さらに追加の指示や対話を重ねることで、穴を埋めたり参照を整えたりして、論文を短時間で何度も書き直して改善できたことを興味深い進歩と捉えました。

タオ氏は、重要な部分は人間が主体的に書く形が望ましいとしているものの、従来は読みやすい原稿を1本仕上げるだけでも大きな労力がかかり、その後の改稿も局所的な修正にとどまりがちだったのに対し、AIを使うと大きな構成変更を含む書き直しを素早く反復できてしまうことを高く評価しています。