AIが数学の未解決問題を解く流れは加速するのか｜「答えが出る速さ」と「数学として認められる速さ」の違い

公開日

2026年9月23日

更新日

2026年9月23日

AIが数学の未解決問題を解いた、というニュースが増えています。2026年9月には、OpenAIが社内の新しいモデルで数学の長年の未解決問題を100件以上解決したと発表しました。こうした流れはこれからも加速するのか。この記事の見立てを先に書くと、AIが「解の候補」を出す速さは今後も上がると考えられますが、その解が数学界で認められるまでの時間も同じように短くなるとは限りません。未解決だったかの確認、証明の検証、数学界に受け入れられるまでの過程という、人の手を通る工程にも時間がかかるからです。以下では、これまでの経緯を加速の判断材料として押さえたうえで、「AIがN件解決」というニュースを読むときの考え方を、確率の計算も交えて整理します。

この記事の主な内容

AIはコンテスト問題と未解決問題の双方で成果を出してきました

ここ数年の主な出来事と、結果がどのように確かめられたかを表にまとめました。

時期	出来事	確かめられ方
2023年12月	Google DeepMindのFunSearchが、8次元のキャップセット問題でそれまでの最大511要素を上回る512要素の例を発見	Nature掲載の論文。例は計算機で正しさを確認できる
2024年7月	AlphaProofとAlphaGeometry 2が国際数学オリンピック（IMO）2024で6問中4問を解き、42点満点中28点の銀メダル相当	AlphaProofは証明をLeanで記述。ティモシー・ガワーズ氏らが採点。1問に最大3日かかった
2025年5月	AlphaEvolveを50以上の未解決問題に適用し、約75%で既知の最良の結果を再発見、約20%で改善。11次元のキッシング数の下界を593に更新	見つけた構成や式を自動で評価する仕組みで確認
2025年7月	Gemini Deep ThinkがIMO 2025で6問中5問を解き35点の金メダル相当。OpenAIの実験モデルも35点相当と発表	Geminiは大会の採点担当者が公式に採点・認定。OpenAIは元メダリスト3人による採点で、公式の認定ではない
2025年10月	OpenAIの幹部が「GPT-5が未解決のエルデシュ問題10件の解を見つけた」と投稿し、のちに削除	既存の文献を見つけただけだったと、問題集サイトの運営者が指摘
2026年9月	OpenAIがナビエ・ストークス方程式の懸賞問題の解決を主張し、論文とLeanによる形式化を公開。続いて「100件以上の未解決問題を解決」と発表	クレイ数学研究所は審査を急がない方針。100件は問題の一覧も証明も非公開（2026年9月時点）

IMOでは、2024年には解答に最大3日かけて銀メダル相当だった水準が、翌2025年には各日の4.5時間の制限内に解答し、金メダル相当に届きました。IMOの成績と解答時間には、1年間で改善が見られました。

加速しているのは「答えの候補を出す」工程です

加速が起きやすいのは、出てきた答えを計算機がすぐに確かめられる問題です。FunSearchやAlphaEvolveが扱ったのは、見つけた構成が条件を満たすか、既存の記録より良いかをプログラムで判定できる種類の問題でした。判定が自動でできれば、AIは候補を大量に出し、良いものだけを残す試行を休まず繰り返せます。計算資源が増えるほど試せる数も増えるので、この種の問題で成果が積み上がっていくのは自然な流れです。

証明そのものが答えになる問題でも、形式検証が同じ役割を果たし始めています。Leanのような証明支援系は、証明を計算機が一歩ずつ検査できる形に書き直し、論理の飛躍がないかを機械的に確かめます。AlphaProofは証明をLeanで記述し、形式化された命題の推論を検査しましたし、2026年9月のナビエ・ストークス方程式の件でも、論文と一緒にLeanでの形式化が公開されました。

一方で、AIが出す候補が増えるほど、それを確かめる側の仕事も増えます。候補を出す速さと、それが数学の成果として確定する速さは、別々に考える必要があります。

未解決問題の解決を評価する3つの関門

未解決問題を解いたという主張を評価する際には、性質の違う3つの確認が必要です。まず、その問題が本当に未解決だったか。次に、証明が正しく、しかも問題が問うていることそのものを示しているか。最後に、ほかの数学者が証明を読み、理解し、自分の手で組み立て直して受け入れるかです。「答えが合っている」は、このうち真ん中の関門だけの話です。

関門	確かめること	主な手段	AIで速くなるか
未解決だったか	既存の文献で解かれていないか	文献調査、専門家による確認	文献探索は速くなるが、最終判断は専門家
証明は正しいか	論理に誤りがなく、問題どおりの命題を示しているか	形式検証（Leanなど）、査読	形式化した証明の推論を機械的に検査できる
数学として受け入れられるか	人が理解し、再構成し、次の研究に使えるか	論文化、査読、追試や別証明	人が読んで理解する時間は短くしにくい

最初の関門でつまずいた例が、2025年10月のエルデシュ問題の件です。TechCrunch（2025年10月19日）によると、OpenAIのケビン・ワイル氏が「GPT-5が未解決だったエルデシュ問題10件の解を見つけ、さらに11件で進展を得た」と投稿しました。ところが問題集サイト erdosproblems.com を運営する数学者トーマス・ブルーム氏は、サイト上の「未解決」は自分がそれを解いた論文を知らないという意味にすぎず、GPT-5は自分の知らなかった既存の文献を見つけたのだと指摘しました。投稿は削除され、10件はどれも新しく解かれたものではありませんでした。

真ん中の関門は、形式検証で機械に任せられる部分が増えています。ただし機械が保証するのは「書き下した命題が証明された」ところまでで、その命題が元の問題を正しく写しているかは人が確かめる必要があります。Anthropicがフェルマーの最終定理を形式化した件でも、定理の書き写しがMathlibの定義と一致しているかの確認が検証手順に含まれていました（Claudeがフェルマーの最終定理を11日で形式化した件で詳しく扱いました）。

最後の関門は、仕組みの上でも時間がかかるようにできています。クレイ数学研究所のミレニアム懸賞の規定では、解が評価の確立した査読付きの出版物に掲載され、掲載から少なくとも2年が経ち、世界の数学界で広く受け入れられることが条件です。ナビエ・ストークス方程式の件では、Leanによる形式化まで公開されていても、同研究所は2026年9月11日の声明で「どうやら解決されたようだ」と書きつつ、審査は「あえて急がない」としています。AIがどれだけ速く証明を書いても、数学界での評価には、専門家が証明を確認する時間がかかります。

「AIがN件解決」は、関門の通過率を掛け合わせて読みます

今後も「AIが未解決問題をN件解決」というニュースは出てくるはずです。そのとき、N件のうち何件が数学の成果として残りそうかは、確率で見積もれます。1件の主張が3つの関門をすべて通る確率は、確率の乗法定理から次のように書けます。

P(全関門を通過) ＝ P(未解決だった) × P(証明が正しい｜未解決だった) × P(受け入れられる｜未解決かつ正しい)

2つ目と3つ目の因子は、前の関門を通ったという条件のもとでの確率、つまり条件付き確率です。もともと既知だった問題の証明は新しい成果として数えないので、最初の関門を通ったものだけを次に回します。N件それぞれの通過確率を足すと、残る件数の期待値になり、通過率がどの件でも同じなら N × P(全関門を通過) です。

2026年9月の「100件」を例に、通過率を3通りに置いて計算してみます。数字はすべて筆者が置いた仮定で、OpenAIや数学者が示したデータではありません。

仮定のシナリオ	未解決だった	証明が正しい	受け入れられる	100件のうち残る期待件数
楽観的な仮定	0.95	0.95	0.9	約81件
中間の仮定	0.8	0.9	0.7	約50件
慎重な仮定	0.5	0.8	0.5	20件

楽観的な仮定でも、それぞれ9割以上の関門を3つ重ねると2割近くが落ちます。この例では、通過率が1未満の関門を追加するたびに、残る期待件数は減ります。また、ほかの通過率を固定して1つを同じ幅で上げるなら、もとの通過率が低い関門ほど期待件数の増加は大きくなります。慎重な仮定で最初の関門を0.5から0.8に上げるだけで、期待件数は20件から32件に増えます。エルデシュ問題の件では、この最初の関門の通過率が10件中0件でした。このため、企業の外から既存研究との重複を確かめることが欠かせません。

もう1つ注意があります。同じモデルが似た手法で出した結果は、互いに独立とは限りません。文献調査の見落としのような系統的な誤りがあれば、多くの件がまとめて落ちます。期待件数は同じでも、共通の原因によって成否が連動すれば、実際の件数のばらつきは独立な場合より大きくなりえます。件数Nだけでなく、各関門の通過率をどこまで外から確かめられるかも、ニュースを評価するうえで重要です。数字を条件ごと読む姿勢は、ベンチマークの読み方を扱った「AGIテストで99.9%」の裏側とも共通しています。

今後のニュースは、公開の範囲と第三者の反応で見分けられます

関門の考え方を使うと、新しいニュースを見たときに確かめる点も自然に決まります。まず見るべきは、どこまで公開されたかです。件数だけなのか、問題の名前まで出ているのか、証明や論文まで読めるのか。問題の名前が出ていなければ、最初の関門の確認すら始められません。2026年9月の「100件」は、OpenAIの発表の時点では件数の主張だけで、問題の一覧も証明も示されていませんでした。

次に、形式検証の有無です。Leanなどで形式化されていれば、証明の論理については信頼度が大きく上がります。そのうえで、形式化された命題が元の問題と一致しているかを誰かが確認したかどうかが残ります。

そして、その分野の専門家や、問題を管理している人がどう反応したかです。エルデシュ問題の件で誤りを指摘したのは問題集サイトの運営者でしたし、ナビエ・ストークス方程式の件ではクレイ数学研究所が慎重な姿勢を示しました。2026年9月には、数学者9人が独立の諮問グループ「AGMAI（Advisory Group on Mathematics and Artificial Intelligence）」を立ち上げ、OpenAIに成果の評価や公表の進め方を助言し始めています。ただしグループ自身が声明（2026年9月21日）で書いているとおり、助言はしても企業の決定に対する権限は持っていません。

“Although we will give advice, we do not have decision making power at any AI company, and the responsibility for the decisions made by any company will rest with that company.”

和訳は「私たちは助言はするが、どのAI企業に対しても意思決定の権限を持たない。企業が下す決定の責任は、その企業が負う」です。同じ時期には、フィールズ賞受賞者らが宣言「A Severe Misalignment of AI in Mathematics（数学におけるAIの深刻なずれ）」を公表し、問題を解くことは概念的な理解のための手段にすぎず、文献の確認や新しい手法の取り出しが追いつかないまま結果が量産されることへの懸念を示しました。専門家の確認が追いついているかどうかが、そのニュースを成果として数えてよいかの目安になります。

よくある質問

AIは数学者の仕事を置き換えますか？

証明の候補を出す部分はAIが担う割合が増えていきそうですが、問題が本当に新しいかの見極め、証明の命題が元の問題と一致しているかの確認、証明を理解して数学の体系に組み込む作業は、いまのところ数学者が担っています。AIが候補を多く出すほど、こうした確認と意味づけの仕事の比重は大きくなると考えられます。

Leanなどの形式化とは何ですか？

証明を、計算機が一歩ずつ正しさを検査できる形式言語で書き直すことです。Leanはそのための代表的な証明支援系で、数学の定義や定理を集めたライブラリMathlibが整備されています。Leanの検証が通れば、定義や公理に基づく推論を機械的に確認できますが、書き下した命題が元の問題を正しく表しているかは人が確かめる必要があります。

ミレニアム懸賞問題はAIで解けたのですか？

2026年9月時点では確定していません。OpenAIはナビエ・ストークス方程式の問題について、解が有限時間で特異点を持ちうることを示したと主張し、論文とLeanによる形式化を公開しました。クレイ数学研究所は「どうやら解決されたようだ」としつつ審査を急がない方針で、規定上も掲載から2年以上と数学界での広い受容が懸賞の条件です。

AIが数学で確実に成果を出した例はありますか？

答えを計算機で確かめられる問題では、第三者が検証できる形の成果が出ています。FunSearchによるキャップセット問題の新しい例はNatureに掲載され、AlphaEvolveは11次元のキッシング数の下界などを更新しました。いずれも、見つけた構成が条件を満たすか計算機で確認できる種類の結果です。

「AIが未解決問題を解いた」というニュースは、それだけでは確率計算の出発点にすぎません。どの問題が本当に新しかったのか、証明は問題どおりの命題を示しているのか、人が理解できる形になっているのか。一つずつ確かめることで、発表された件数をどう評価すべきか判断できます。条件付き確率や証明の考え方を学び直す際には、こうしたニュースを題材にできます。和からの生成AIに必要な数学個別指導では、確率やベクトルといった数学を、AIを使っていて湧いた疑問から逆算して学び直せます。

参考にした資料
・Romera-Paredes et al.「Mathematical discoveries from program search with large language models」（Nature、2023年12月14日）
・Google DeepMind「AI achieves silver-medal standard solving International Mathematical Olympiad problems」（2024年7月25日）
・Google DeepMind「AlphaEvolve: A Gemini-powered coding agent for designing advanced algorithms」（2025年5月14日）
・Google DeepMind「Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad」（2025年7月21日）
・Engadget「OpenAI’s experimental model achieved gold at the International Math Olympiad」（2025年7月19日）
・TechCrunch「OpenAI’s embarrassing math」（2025年10月19日）
・OpenAI「On the Navier–Stokes Millennium Prize Problem」（2026年9月8日）
・Clay Mathematics Institute「Navier-Stokes Announcement」（2026年9月11日）
・Clay Mathematics Institute「Rules for the Millennium Prizes」（PDF）
・OpenAI「Advisory Group on Mathematics and AI」（2026年9月21日）
・AGMAI「Advisory Group on Mathematics and Artificial Intelligence」（テレンス・タオのブログへのゲスト投稿、2026年9月21日）
・「A Severe Misalignment of AI in Mathematics」（2026年9月11日）／テレンス・タオによる解説