数学未解決問題、AI単独で続々解決。フィールズ賞数学者が考えるAI証明の実態を「エルデシュ問題」から読み解く（生成AIクローズアップ）

1週間の気になる生成AI技術・研究をいくつかピックアップして解説する連載「生成AIウィークリー」から、特に興味深いAI技術や研究にスポットライトを当てる生成AIクローズアップ。

今回は、フィールズ賞受賞者であるテレンス・タオ教授が管理するGitHubページ「AI contributions to Erdős problems」を取り上げます。

このページでは、AIツールが数学の難問「エルデシュ問題」にどのような貢献をしてきたかが体系的に記録されています。エルデシュ問題とは、20世紀を代表する数学者ポール・エルデシュが提起した数多くの未解決問題群です。

▲（左）ポール・エルデシュ、（右）当時10歳のテレンス・タオ（Wikipediaより引用）

このページには、AIによって完全に解決された問題、部分的な進展が見られたもの、あるいは進展が見られなかった事例が集約されており、それぞれの成果は緑（完全解決）、黄（部分的解決）、赤（進展なし）のアイコンを用いて可視化されています。

またAIの貢献をいくつかのカテゴリーに分類して整理しています。完全にAIが生成した解でその後の文献調査でも先行研究が見つからなかったもの、AIが解を導いたものの実は既存の文献に同等の結果があったもの、人間の数学者とAIの協働による成果などです。

▲タオ氏が管理するGitHubページ

AIによる解決成果をどう評価するか

このページにおいて強調されているのは、単なる解決数のリストアップではなく、AIによる成果をどのように評価し、数学的知識として統合していくかという極めて慎重かつ学術的な視点です。

掲載されている成果を評価するにあたっては、いくつかの重要な留保が必要です。まず、エルデシュの問題は1000以上あるとされており、その難易度が異なり、現在のAIにとって解きやすい問題から超難問までが混在しているため、単なる解決数の多寡だけで特定の手法の優劣を論じることはできません。

また、ページ上で「未解決」と分類されていても、AIが解いた直後に実は過去の文献で人間によって解決済みであったことが判明するケースも多発しています。これはAIが過去の文献を学習していた可能性があり、単にその問題が長らく注目されてこなかったために文献が見過ごされていたケースもあります。

そもそもAIが解を出力したとしても、それが訓練データに含まれていた既存文献の影響を受けているのか、あるいは独立に同じ結論に達したのかを判断することは難しいです。

さらに、AIによる解決は、人間が執筆する論文のような「数学的な洞察」や「他分野との関連性」といった文脈的価値を欠いていることが多く、単に証明が正しいというだけでは数学的価値が高いとは限りません。

加えて、Leanなどの証明支援言語による形式化は正当性の保証として有効ですが、問題の定式化そのものの誤りや、証明システムの抜け穴を利用した見かけ上の解決が含まれるリスクにも留意すべきです。

報告バイアスの問題も指摘されています。AIツールを使って問題に取り組んだが進展がなかった場合、そのような失敗例は報告されにくいです。したがって、このページに掲載されている成功例だけを見てAIの成功率を推測することは適切ではありません。

AIの進化により、エルデシュ問題の解決が加速

編集履歴を見ると2025年後半から2026年初頭にかけての更新が頻繁であり、Aristotle、ChatGPT 5.2 Pro、AlphaProof、Geminiといった最新のAIモデルが、数学の難問に対して次々と投入されている現状が読み取れます。

過去の文献にもなく、AI単独で生成した完全解としては、1月10日に発表された問題205番と1月17日に発表された652番が挙げられています。問題205番はAristotleとChatGPT 5.2 Thinkingの組み合わせで、問題652番はGPT 5.2 Proによって解決されました。

　エルデシュ問題をAI単独で解決した初の事例でいうと、プレプリント論文「Resolution of Erdős Problem #728: a writeup of Aristotle's Lean proof」が挙げられます。1月6日にAI単独で問題728番を解決したと述べています。

解決までの過程は次の通りです。1月4日、Kevin Barreto氏がGPT-5.2 ProとAristotleを連携させ、最初の証明を導出しました。しかし当初、解釈の曖昧さが残されており、コミュニティ内ではAIが解いたものがエルデシュの本来の意図と合致しているか疑問視され、あくまで部分的な成果という扱いでした。

翌1月5日、Barreto氏は再びGPT-5.2 Proに、フォーラム参加者が特定した問題の正式な解釈に対応できるか尋ねました。GPT-5.2 Proは可能だと回答し、その議論をもとにAristotleが実行され、1月6日にLean言語による形式的証明が完成しました。先行研究の調査も行われましたが、この問題を解決した既存の文献は発見されなかったということです。

一時は人為的な介入があったのではないかとの誤解も生じましたが、Barreto氏はこれを否定し、純粋にAIのみによる推論であることが確認されました。タオ氏もこの自律性を認めているということです。タオ氏のSNS投稿では「エルデシュ問題の1つ（728番）がAIによってほぼ自律的に解決された」と述べています。

タオ氏が管理するページでは、728番を完全解決としていますが、Pomerance (2014) による部分的結果が見つかり、「AIが自力で解いたが、実は既存の部分的解決があった問題」であり、12月のChatGPT DeepResearchでの文献調査では見つかっていなかったことから、「AIによる事前の文献検索ではその既存研究を見落としていた」という解釈がされています。