AIは「数学の証明」そのものを変えるのか――Lean、未解決問題、そして「問いを構造化する」数学の未来
2026年、数学の世界で興味深い変化が起き始めている。
AIが数学の問題を解く。
それ自体は、もはやそれほど珍しいニュースではない。
数学オリンピック級の問題を解き、プログラムを書き、証明の続きを提案する。生成AIの数学能力が急速に向上していることは、すでによく知られている。
しかし最近、その一段先の動きが目立つようになってきた。
AIが、数学者が実際に研究している未解決問題そのものに入り始めているのである。
その象徴の一つが、数学者ポール・エルデシュが残した膨大な問題群だ。
2026年8月3日、Quanta Magazineは、
「Why the Legendary Erdős Problems Are Falling to AI」
という記事を掲載した。
日本語にすれば、
「なぜ伝説的なエルデシュ問題にAIが迫りつつあるのか」
というところだろう。
しかし、この動きを追っていくと、もっと大きな変化が見えてくる。
AIが数学の難問を解き始めた、というだけではない。
もしかすると、
「数学において証明するとは何なのか」
という、数学研究そのものの構造が変わり始めているのではないだろうか。
エルデシュ問題がAIの実験場になり始めた
20世紀を代表する数学者ポール・エルデシュは、生涯に1500本を超える論文を発表し、多数の数学者と共同研究を行ったことで知られている。
そして彼は、数論、組合せ論、グラフ理論などを中心に、膨大な問題を残した。
その中には解決されたものもあれば、現在も未解決のものもある。
このエルデシュ問題群が、現在AIによる数学研究の重要な対象になりつつある。
理由の一つは、その性質にある。
問題が比較的明確に定義されている。
真偽を判定する対象がはっきりしている。
組合せ論など、計算機による大量探索と相性のよい分野も多い。
そして何より、
「解ければ本当に新しい数学研究になる」
という特徴を持っている。
AIの数学能力を測定するなら、既に答えの分かっている試験問題だけでは十分ではない。
本当に未知の問題を与えなければならない。
エルデシュ問題は、そのための格好の実験場になりつつある。
AIは「証明を書く機械」だけではない
ここで重要なのは、AIの役割を単純な証明作成だけに限定しないことである。
数学研究には、本来いくつもの工程がある。
問題を発見する。
問題の構造を分析する。
既存研究を調べる。
似た問題を探す。
予想を立てる。
反例を探す。
補題を作る。
証明方針を考える。
証明を書く。
そして、その証明が正しいか検証する。
従来、これらの多くを数学者自身が行ってきた。
ところがAIの登場によって、それぞれを別々のシステムが担当できるようになり始めている。
例えばAIは、一つの問題に対して大量の証明方針を生成できる。
あるAIは反例を探す。
別のAIは関連論文を探索する。
さらに別のAIが証明候補を作る。
そしてLeanのような形式証明系が、その論理に誤りがないかを機械的に確認する。
つまり数学研究が、
発見
→ 構造分析
→ 探索
→ 証明生成
→ 形式検証
→ 人間による意味の理解
という工程へ分解され始めている。
Leanとは何か
ここで重要になるのが「Lean」である。
Leanは、数学的な命題や証明をコンピューターが厳密に確認できる形で記述するための形式証明システムである。
通常の数学論文では、人間同士なら理解できる部分について、途中の論理を省略することがある。
しかしコンピューターは、それを「当然」とは理解してくれない。
前提は何なのか。
どの定義を使ったのか。
どの定理から次の式が導かれたのか。
一つ一つ論理的に記述する必要がある。
その代わり、Leanが証明を受理すれば、少なくとも形式化された論理体系の内部では、その証明が正しく組み立てられていることを機械的に検証できる。
難問が提出された瞬間に「形式化」が始まる？
ここからは、現在の研究動向を踏まえた未来予測である。
今後、数学者が重要な予想や未解決問題を提示したとき、その問題に対して早い段階から、
「この問題はLeanでどう表現できるのか」
という作業が行われるようになる可能性がある。
さらに、その前後でAIによる問題構造分析も行われるだろう。
例えば、
どの数学分野に属するのか。
既存のどの定理と接続しているのか。
どの部分が計算可能なのか。
有限の場合を大量探索できるのか。
反例探索が有効なのか。
どの補題へ分解できるのか。
どの部分を形式証明に向けられるのか。
AIによる探索に適した問題なのか。
こうした情報を、問題が提示された早い段階で整理するのである。
すると「未解決問題」という存在そのものが変わってくる。
「問題文」から「構造化された研究対象」へ
従来、未解決問題は基本的には文章や数式として数学者共同体に提示されてきた。
しかしAI時代には、それだけではなくなるかもしれない。
一つの問題に対して、
人間向けの問題文
と同時に、
形式証明系向けの定式化
があり、
さらに、
AI向けの構造情報
が付与される。
例えば、
関連定理、
既知の部分結果、
探索済み領域、
反例が存在しないことを確認した範囲、
有力な証明戦略、
失敗した証明戦略、
必要と考えられる補題、
他の未解決問題との依存関係。
こうした情報が機械可読な形で蓄積されれば、未解決問題は単なる「問い」ではなくなる。
人間とAIが共同探索できる、構造化された研究対象になる。
すると「どの問題をAIに解かせるか」が重要になる
ここで、さらに興味深い問題が現れる。
AIの計算能力には限界がある。
どれほどAIが進歩しても、世界中のすべての数学問題について無限に探索することはできない。
すると、
「どの問題にAIの探索能力を投入するべきなのか」
という問題が生まれる。
単に難しい問題を選べばよいわけではない。
例えば、
解決すると他の多くの問題が前進する問題。
既存理論を大きく拡張する問題。
反例が見つかれば研究方向そのものが変わる問題。
AIの大量探索が特に有効な問題。
形式証明との相性がよい問題。
こうした条件から、AIによる研究の優先順位を考える必要が出てくる。
つまりAIは、
「問題を解く存在」
であると同時に、
将来的には、
「どの問題を解くべきかを分析する存在」
にもなっていく可能性がある。
「証明された」と「理解された」は同じなのか
そして、この変化は数学哲学にも大きな問いを突きつける。
例えば将来、AIがある難問について、人間には到底追い切れない巨大な形式証明を生成したとする。
Leanはそれを完全に正しいと判定した。
では、その問題は「解決した」と言ってよいのだろうか。
論理的には証明されている。
しかし人間の数学者は、なぜその定理が成立するのかを理解していない。
ここで、
「証明されたこと」と「理解されたこと」
が分離する。
数学における証明には、単なる正しさの保証だけではない役割がある。
優れた証明を見ることで、
「なぜそうなるのか」
が分かる。
別の定理との関係が見える。
新しい数学的構造が発見される。
さらに新しい問いが生まれる。
つまり証明とは、真偽を判定するだけではなく、
数学を理解するための装置
でもある。
数学的証明が「機能分化」する時代
そう考えると、現在起きている変化を別の角度から見ることができる。
従来、「証明」という言葉の中に一体化していた知的活動が、
発見
証明
検証
説明
評価
へと分かれ始めているのである。
AIが発見する。
AIが証明候補を作る。
Leanが検証する。
人間とAIが理解可能な説明へ変換する。
そして数学者共同体が、その数学的意味と価値を評価する。
この分業が定着すれば、「数学者の仕事」そのものも変わっていく。
数学者は「証明する人」から「問いと意味を設計する人」へ？
もちろん数学者が証明をしなくなるわけではない。
人間による証明には、数学的直観や美しさ、新しい概念の発見という重要な役割が残る。
しかしAIが探索と形式証明を大量に行えるようになれば、人間の数学者に求められる能力の重心は少しずつ変わるかもしれない。
何を問うのか。
どの問題が重要なのか。
AIに何を探索させるのか。
AIが発見した結果にはどのような意味があるのか。
そこからどのような新しい概念を作るのか。
そして次に何を問うのか。
数学者の役割が、
「答えを見つける人」から、「問いと意味を設計する人」へ
少しずつ広がっていく可能性がある。
おわりに――AIが変えるのは「答え」だけではない
AIがエルデシュ問題を解いた。
AIが新しい反例を発見した。
こうしたニュースだけを見ると、私たちはつい、
「AIは人間より数学が得意になるのか」
という競争の話として考えてしまう。
しかし本当に重要なのは、そこではないのかもしれない。
AIによって変わろうとしているのは、数学者の能力比較ではなく、
数学研究という知的生産システムそのもの
だからである。
問題が提示される。
同時に形式化が始まる。
AIが構造を分析する。
複数のAIが証明と反証を探索する。
形式証明系が検証する。
数学者がその意味を読み解く。
そして、その結果から次の問いが生まれる。
もしこの循環が当たり前になれば、数学研究は大きく姿を変えるだろう。
そして最後に残るのは、おそらく非常に人間的な問いである。
「何を証明できるか」ではなく、「私たちは何を証明したいのか」。
AI時代の数学は、そこを問い始めているのかもしれない。
