数学の未解決問題には、答えへ到達するまで何年、何十年とかかるものがある。時間を要する理由は、最終的な証明を書く作業だけにあるのではなく、その証明へ至る経路を見つけるまでに大きな探索が必要になるためである。どの定理を使うか、どの補題を先に証明するか、どの条件を緩められるか、どの方向が行き止まりかを判断しながら、数学者は多数の可能性から有望な経路を絞り込んできた。
この構造では、証明候補へ到達するまでの探索が研究全体の速度を大きく左右する。正しい証明候補が得られて初めて、その証明の妥当性を確認し、何が新しいのかを理解し、既存の数学との関係を整理できる。探索に長い時間が必要であれば、その後ろにある検証、理解、体系化の工程も開始を待つことになる。
AI が大量の候補を並列に探索し、その成果を形式証明へ変換できるようになると、この順序のうち前半だけを急速に高速化できる。2026 年 9 月には、OpenAI が Navier–Stokes 方程式のミレニアム懸賞問題に対する解決案を公開し、同時に Lean による形式化も公開した。数日前には Anthropic が、フェルマーの最終定理について 1,300 万行の Lean を 11 日で生成し、機械検証可能な証明を構築したと発表している。
ここで変化しているのは、AI が一つの難問へ正答したという事実だけではない。人間が長時間をかけていた探索を大量並列処理へ移し、その出力を形式検証へ接続することで、数学研究の一部を人間の読解速度から切り離せるようになった点にある。証明候補を作る速度と、その正しさを確認する速度がともに上がれば、研究全体を制限する工程はさらに後ろへ移る。
既稿では、フェルマーの最終定理の形式化を題材に、AI が成果物を生成することと、その成果物を正しいと確定することを分けて考えた[1]。形式検証を使えば、生成した AI 自身の判断だけに正しさを委ねず、別の検証機構によって成果物を確定できる。これは、大量生成された証明を扱ううえで大きな意味を持つ。
しかし、正しさが確定した時点で数学上の処理がすべて完了するわけではない。その証明の中心的な考え方は何か、どの概念が別の問題にも使えるか、従来の理論をどこまで拡張したのか、どの表現へ圧縮すれば他の数学者が利用できるのかという工程が続く。形式検証が扱う「正しいか」と、人間が扱う「何を意味するか」には異なる完了条件がある。
AI によって数学的な答えを生成するコストが低下すると、数学で希少になるものは答えそのものから、その答えを選び、理解し、体系化し、次の知識へ接続する能力へ移る。生成能力が増えた結果として数学者の仕事が単純に減るのではなく、数学研究の中で全体速度を決める場所が移動する。本稿では、この律速段階の移動を考える。
1. 答えを作ることが最も難しいとは限らなくなる
複数の工程からなる仕事では、一つの工程だけを高速化しても、全体の処理量が同じ倍率で増えるとは限らない。工場で部品を作る工程を 10 倍速くしても、次の組み立て工程が従来と同じ速度なら、部品が組み立て工程の前に蓄積する。最終的な生産量を決めるのは、最も速くなった工程ではなく、処理待ちを生じさせている工程である。
数学研究にも同じ構造がある。問題を解く活動を単純化すると、「候補を生成する」「正しさを検証する」「意味を理解する」「既存知識へ体系化する」という少なくとも 4 つの工程に分けられる。それぞれは前の工程から成果物を受け取るが、完了条件は異なる。
| 工程 | 完了条件 | 次工程へ渡されるもの |
|---|---|---|
| 生成 | 問題に対する証明候補や反例候補が得られる。 | 正しさを確認できる候補成果物が渡される。 |
| 検証 | 候補が定められた論理体系や検証条件を満たすことが確認される。 | 正しさが確定した成果物が渡される。 |
| 理解 | 証明の中心的な考え方、成立条件、再利用可能な概念を説明できる。 | 人間が別の問題でも扱える概念や方法として整理された知識が渡される。 |
| 体系化 | 既存理論との関係、適用範囲、派生結果、次の研究課題が位置付けられる。 | 数学共同体が参照し、再利用し、発展させられる知識体系へ統合される。 |
従来の研究数学では、多くの難問で最初の生成工程が主要な制約だった。証明候補そのものが存在しなければ、その証明が正しいかを検証する対象も存在しない。検証済みの成果がなければ、その成果から新しい概念を抽出し、既存理論へ位置付ける作業も進みにくい。このため、正しい探索経路を見つけて問題を解く能力が長く希少資源になってきた。
生成工程が高速化すると、この依存関係の後半が目立つようになる。たとえば 1 年に 1 件しか新しい証明候補が得られない状況では、人間がその 1 件を時間をかけて検証し、理解する余地がある。AI が同程度の証明候補を短期間に大量生成する状況では、人間側の検証能力が同じままなら候補が検証待ちとして蓄積する。形式検証によって検証まで高速化すれば、今度は検証済み成果が理解待ちとして蓄積する。
この移動はソフトウェア開発でも起きる。コードを生成する速度が上がっても、生成物を採用可能な状態へ確定するには、仕様との照合、テスト、レビュー、依存関係の確認といった別工程が必要になる。既稿では、テスト通過が保証する範囲と仕様全体の充足を分けて考える必要があることを整理した[2]。さらに、AI に仕事を任せる場合には、モデルの外側へ観測、操作、検証の仕組みを置き、生成物を確定済み成果へ変換する必要がある[3]。
生成量そのものが増えると、もう一つの変化が起きる。未検証、回答待ち、依存関係待ちといった状態も生成量に比例して増えるため、各成果物がどの状態にあるのかを管理しなければ、生成量の増加がそのまま完成量の増加へつながらない。既稿では、AI による大規模開発で未確定な状態を一件ずつ閉じる必要性を、この構造として整理した[4]。
数学でも、証明候補の生成量が増えれば同じ構造が現れる。生成された証明候補を検証済みへ変え、さらに人間が理解可能な概念へ変え、既存理論へ統合する必要がある。前の工程だけが高速化すると、成果物は次の工程の入口へ蓄積する。
このため、AI による数学研究の変化を評価するときには、何問を解いたかだけを見ると全体像を取り違える。生成、検証、理解、体系化のうち、どこまで処理能力が増え、どこに処理待ちが移ったのかを見る必要がある。証明生成が十分に高速化した世界では、問題を解く能力そのものより、その後ろに残された工程が数学全体の速度を決め始める。
2. 生成、検証、理解、体系化は別の仕事である
前章で分けた 4 つの工程を、今度は処理時間として考える。証明候補を生成する時間を \(T_g\)、正しさを検証する時間を \(T_v\)、人間が数学的な意味を理解する時間を \(T_u\)、既存知識との関係を整理して体系化する時間を \(T_i\) とする。
| 記号 | 工程 | 時間を要する主な作業 |
|---|---|---|
| \(T_g\) | 生成 | 証明方針を探索し、補題を組み合わせ、成立する証明候補や反例候補へ到達する。 |
| \(T_v\) | 検証 | 候補が論理的に成立し、前提や定義を満たしていることを確認する。 |
| \(T_u\) | 理解 | 証明を成立させている中心的な考え方を抽出し、なぜ成立するのかを人間が説明可能な形にする。 |
| \(T_i\) | 体系化 | 既存理論との関係、適用範囲、一般化可能な部分、派生する問題を整理し、再利用可能な知識として位置付ける。 |
最も単純な直列モデルとして書けば、一つの成果が生成されてから体系化されるまでの時間は次のように表せる。
\[
T_{\mathrm{total}} = T_g + T_v + T_u + T_i
\]
実際の数学研究は、この式のように一方向へ進むだけの処理ではない。証明を理解する途中で誤りが見つかれば検証から生成へ戻り、既存理論との関係を整理する過程で新しい補題が必要になれば、再び探索が始まる。体系化によって新しい未解決問題が生まれることもある。この式は研究活動そのものを完全に記述するモデルではなく、各工程に別々の処理時間が存在することを見るための分解である。
従来の難問では、しばしば \(T_g\) が他の工程より大きかった。証明候補へ到達するまでに何年も必要なら、その期間は検証対象そのものが存在しない。候補が得られて初めて正しさを確認でき、正しいと判断された成果から概念を抽出し、既存の数学へ組み込む作業が始まる。このため、生成工程の長さが研究全体の進行速度を強く制約していた。
AI による大量並列探索は、この \(T_g\) を縮める方向に働く。さらに、生成された証明を Lean のような形式証明系へ変換できれば、正しさを確認する \(T_v\) も人間の逐語的な読解だけに依存しなくなる。前半の 2 工程が短縮されれば、同じ成果一件について見たとき、理解と体系化が全体時間に占める割合は相対的に大きくなる。
\[
T_g \downarrow,\quad T_v \downarrow
\quad\Longrightarrow\quad
\frac{T_u + T_i}{T_{\mathrm{total}}} \uparrow
\]
この式が表しているのは、人間が一つの証明を理解するための時間 \(T_u\) 自体が増えるという意味ではない。生成と検証だけが高速化すれば、それまで \(T_g\) と \(T_v\) に隠れていた \(T_u\) と \(T_i\) が、研究全体の処理時間を決める要因として前面に出るという意味である。
さらに成果の生成量まで増えると、問題は一件当たりの時間配分だけでは済まなくなる。たとえば AI が短期間に 100 件の検証済み証明を供給し、人間側が同じ期間に 10 件しか十分に理解できなければ、90 件は理解待ちとして残る。生成と検証の処理能力が上がるほど、その出力を受け取る理解工程の処理能力との差が蓄積量として現れる。
ここで「AI が答えを出した」という表現を工程へ分解すると、状態の違いが見える。証明候補が生成された状態、形式体系が受理した状態、その証明の意味を人間が説明できる状態、さらに数学共同体がその知識を別の研究で再利用できる状態には、それぞれ別の完了条件がある。
この区別によって、AI による数学研究の高速化を単なる正答数の増加として見る必要がなくなる。生成と検証が高速化した後に理解と体系化の処理量が追いつかなければ、検証済みでありながら十分に消化されていない数学が蓄積する。AI が数学研究の前半を高速化するほど、後半の工程が研究全体の速度を決める構造が明確になる。
3. AI は未解決問題を解く速度を変え始めた
AI と数学の関係は、2022 年から 2026 年までの数年間で対象そのものが変化した。2022 年に OpenAI が公開した形式数学の研究では、Lean 上で高校数学オリンピック級の問題を解くニューラル定理証明器が中心だった。miniF2F ベンチマークでは当時の最高水準となる 41.2% を記録した一方、OpenAI 自身も最高水準の学生にはまだ遠いと説明していた[5]。この段階では、正解がすでに知られている問題を形式体系の中でどこまで自動的に解けるかが主要な評価軸だった。
既知の正解を持つ問題は、AI の性能を測る対象として扱いやすい。生成された証明が正しいかを既知の結果と照合でき、複数のモデルを同じ問題集合で比較できるからである。一方、この方法で測れるのは、あらかじめ人間が問題と解答を用意した範囲での能力である。研究数学へ進むには、正解が存在することも、どの方向へ探索すればよいかも分かっていない状態から成果を作る必要がある。
2026 年 5 月には、その境界を越える事例が現れた。OpenAI の内部モデルは、Erdős の単位距離問題に関する長年の予想に対して反例となる無限族の構成を発見した。これは、単位距離を持つ点の組を最大化する構成について有力だった見方を破る結果であり、その後、外部の数学者による確認も行われた[6]。
この事例では、AI が既知の証明を再現したのではなく、事前に正解が登録されていない問題空間から新しい構成を探索している。評価方法も変わる。ベンチマークなら正答表との比較で性能を測れるが、未解決問題では、生成された結果そのものを数学者が検証し、新しい数学的成果として成立するかを判断する必要がある。AI の出力が評価対象から研究成果候補へ変わることで、生成後の検証工程まで研究活動の一部になる。
8 月には規模がさらに拡大した。OpenAI は、数学と理論計算機科学の長年の未解決問題 10 件について、解決または実質的進展を公表した。対象には高次元球充填、符号理論、非 sofic 群、Connes の剛性予想、算術回路複雑性、量子並列反復、格子暗号に関係する最近ベクトル問題などが含まれる。分野ごとに必要な専門知識や証明技法が異なる問題群に対して、内部版 Astra が成果を生成し、後に各議論が Lean の証明書へ形式化されたと報告されている[7]。
ここでは一件の難問を偶発的に解いたという段階から、複数分野の未解決問題を継続的な探索対象として処理する段階へ進んでいる。対象数が増えると、AI の能力を見る尺度も変わる。一つの有名問題を解けるかという評価より、異なる数学分野で未解決問題を探索し、検証可能な成果へ変換する処理能力が重要になる。
同じ時期には Anthropic でも、未公開版 Claude が Riemann ゼータ関数に関する既存の下界を改善した。Riemann 予想そのものの証明ではなく、予想を満たす零点の割合に関する下界を 41.6% から 67.2% へ引き上げたという成果である[8]。完全解決に到達していない場合でも、既知の数学的境界を更新できれば研究成果になる。この点でも、正解済み問題を解くベンチマークとは評価構造が異なる。
2022 年から 2026 年までの変化を並べると、AI 数学の対象が段階的に外側へ広がっていることが分かる。既知の問題を形式体系上で解く段階から、未解決問題に新しい反例や証明を与える段階へ進み、さらに複数分野の研究課題を並列に探索する段階へ移っている。
| 段階 | 主な対象 | 成果の判定方法 | 研究工程への影響 |
|---|---|---|---|
| 既知問題の自動証明 | 正解が既知の数学オリンピック級問題などを扱う。 | 既知の正解や形式検証によって性能を評価できる。 | 主として証明生成能力の評価として機能する。 |
| 未解決問題への新成果 | 正解が事前に存在しない研究数学の問題を扱う。 | 生成後に数学者や形式体系による独立した検証が必要になる。 | AI の出力が研究成果候補として扱われる。 |
| 複数分野の継続的探索 | 異なる数学分野にまたがる未解決問題群を扱う。 | 問題ごとに証明、反例、既存境界の改善など異なる基準で評価する。 | 生成だけでなく、検証、選別、理解まで含む後続工程の処理能力が必要になる。 |
この変化によって、AI 数学の評価対象は単一のベンチマーク得点から研究工程そのものへ移りつつある。既知問題では、生成速度が上がっても処理すべき問題集合にはあらかじめ境界がある。未解決問題では、AI が新しい成果を生成するたびに、その成果を検証し、重要性を評価し、数学的意味を理解する仕事が新たに発生する。
つまり、未解決問題を解く速度が上がることは、単に研究成果が早く得られることだけを意味しない。生成能力が研究数学の供給量を増やすことで、後続する検証、理解、体系化へ渡される成果物の量も増える。2026 年 9 月の Navier–Stokes 方程式の事例では、この構造が一件の成果を超え、約 1 万の並列エージェントを使った大規模探索として現れる。
4. Navier–Stokes では約 1 万の並列エージェントが探索した
前章で見た未解決問題への進出が、どの程度の計算規模で起きているのかを具体的に示すのが、2026 年 9 月 8 日に OpenAI が公表した Navier–Stokes 方程式のミレニアム懸賞問題に対する解決案である。OpenAI は、内部モデルを用いた多数の協調エージェントに複数の問題設定を並列探索させ、そのうち Navier–Stokes の解決案へ到達したグループは、およそ 1 万の同時並列エージェントから構成されていたと報告している[9]。
探索に投入された規模は、エージェント数だけではない。最初のエージェントを起動してから解決案へ到達するまで約 88 時間を要し、その後 GPT-6 Astra を用いて Lean へ形式化し、検証可能な状態へ移すために追加で 17 時間を要した。Navier–Stokes の探索だけで約 270 万件のメッセージと約 1,300 億出力トークンが使われたとされる[9]。
この数字は、AI が人間一人の思考を単純に高速再生している状況とは異なることを示している。約 1 万のエージェントが異なる方向を同時に探索できるため、一つの方針を試して失敗してから次へ進む逐次的な探索を、大量の並列探索へ変換できる。さらに、その探索で得られた証明候補を Lean へ渡すことで、生成と検証を別工程として連続して処理している。
| 工程 | OpenAI の公表値 | 研究工程上の意味 |
|---|---|---|
| 探索規模 | 解決案へ到達したグループは約 1 万の同時並列エージェントで構成された。 | 候補となる証明方針を、一人の研究者が順番に試す場合とは異なる並列度で探索できる。 |
| 解決案への到達 | 最初のエージェント起動から約 88 時間を要した。 | 長期間未解決だった問題に対して、大量の探索を数日間へ集中させる処理が成立している。 |
| 形式化と検証 | GPT-6 Astra により追加で 17 時間を要した。 | 証明候補の生成後に、その内容を形式体系へ移し、機械検証可能な成果物へ変換する別工程が存在する。 |
| 探索出力量 | 約 270 万件のメッセージと約 1,300 億出力トークンを使用した。 | 最終論文の背後に、人間が逐語的に追跡することを前提としない規模の探索過程が存在する。 |
大量探索の結果として公開された論文は、滑らかな初期条件と滑らかな外力を与えた場合に、Navier–Stokes 方程式の解へ有限時間で特異点が生じる構成を提示している[10]。ここで外力が含まれることは、成果の位置付けを理解するうえで重要である。Clay Mathematics Institute の公式問題文には複数の解決条件が定義されており、全空間 \(\mathbb{R}^3\) における解の破綻を示す選択肢 C と、周期的トーラス \(\mathbb{R}^3/\mathbb{Z}^3\) における破綻を示す選択肢 D が含まれている[11]。
OpenAI は、今回の構成がこの C と D を成立させると説明している。公開された Lean リポジトリーでも、全空間と周期的トーラスについて、それぞれ滑らかな初期条件と外力の下で大域的な滑らかな解が成立しないことを形式化し、公式問題文の C、D との対応を明記している[12]。つまり、AI が探索したのは周辺的な補題ではなく、ミレニアム懸賞問題であらかじめ定められていた解決条件そのものへ対応する構成である。
この事例から確認できる変化は、モデル単体の能力順位よりも研究工程の処理方式にある。約 1 万のエージェントによって探索空間を並列処理し、約 88 時間で証明候補へ到達し、さらに 17 時間で形式検証可能な成果物へ変換した。生成工程と検証工程の両方を大規模な計算処理へ移せるようになると、従来は人間の探索時間によって制限されていた数学研究の前半部分を、別の時間尺度で処理できる。
同時に、この規模は次の制約も生む。最終的な成果物だけを見れば一つの論文と一つの形式証明であるが、その背後には約 1,300 億出力トークンに及ぶ探索がある。人間がその探索過程を最初から最後まで読み直して妥当性を判断する方式は、この処理量に対応しにくい。生成能力がこの規模へ到達したことで、次に必要になるのは、膨大な探索過程そのものを読むことではなく、そこから得られた成果を独立した方法で検証できる仕組みである。
5. 大量生成された証明は形式検証へ渡せる
前章で見たように、AI が数百万件のメッセージや数千、数万の探索主体を使って証明候補を生成するようになると、人間が探索過程そのものを最初から最後まで読み直して正しさを確認する方法は処理量に追随しにくくなる。生成能力が増えれば、検証すべき成果物の量も増えるため、次に全体の速度を制約するのは検証工程である。
人間が一つの数学証明を検証するときには、結論だけを見るわけではない。各式変形が成立するか、利用した補題の前提条件を満たしているか、定義の適用範囲を逸脱していないか、暗黙に置かれた仮定が結論へ影響していないかを順番に確認する。証明が短く、生成される件数も少なければ、この方法で対応できる。証明が巨大化し、さらに多数の証明が短期間に生成されると、人間が読み終えるまでの時間が生成時間を上回る。
2026 年 9 月に Anthropic が公表したフェルマーの最終定理の形式化は、その規模を具体的に示している。Claude は主として自律的に 11 日間動作し、定理の前提から結論までを機械検証できる Lean の証明を構築した。生成された Lean は約 1,300 万行に達し、作業中には 30,300 個の定理が証明され、そのうち約 29,500 個が最終的な証明で利用された[13]。
| 対象 | Anthropic の公表値 | 検証工程上の意味 |
|---|---|---|
| 作業期間 | Claude が主として自律的に 11 日間動作した。 | 巨大な形式証明を、人間が同じ速度で逐語的に確認することを前提としない生成工程が成立している。 |
| Lean の規模 | 生成されたコードは約 1,300 万行に達した。 | 証明の正しさを人間の読解量だけで支える方式では、生成速度との処理量差が大きくなる。 |
| 証明された定理 | 作業中に 30,300 個の定理を証明した。 | 最終定理へ到達するまでに、多数の中間成果を生成しながら証明体系を構築している。 |
| 最終証明で利用された定理 | 約 29,500 個が最終証明に組み込まれた。 | 最終成果の検証には、巨大な依存関係全体の整合性を確認する必要がある。 |
1,300 万行を人間が一行ずつ読み、30,000 個規模の定理について依存関係を確認する方法では、11 日間という生成速度に追随することが難しい。ここで Lean の役割が生じる。Lean では数学の命題を型として表し、その命題の証明を対応する型の項として表現する。最終的にはカーネルが、与えられた証明項が要求された型を持つかを検査する[14]。
たとえば「ある命題 \(P\) が真である」という主張を Lean 上の型 \(P\) として定義すると、その証明は \(P\) 型を持つ項として表される。証明を生成した AI が「正しい」と自己評価することより、Lean のカーネルがその項を受理することが最終的な判定条件になる。証明を作る主体と、証明を受理する主体を分離できる。
この分離は、AI による大量生成との相性がよい。AI が探索中に多数の失敗、行き止まり、不完全な補題を生成しても、それらすべてを人間が精読する必要はない。最終的に形式体系が受理した証明を確定済み成果として区別し、受理されなかった候補を排除できる。生成量を増やすことと、人間が同じ量を確認することを切り離せる。
形式証明系が保証する範囲も明確である。Lean が確認するのは、形式化された定義、公理、既証明定理の下で、最終的な命題が論理的に導出されているかという点である。このため、自然言語で書かれた証明の雰囲気や AI の説明能力ではなく、明示された形式体系の内部で成立する導出を検証対象にできる。
この構造を前章までの工程へ戻すと、AI による数学研究では二つの処理能力が連続して増えている。大量並列探索によって証明候補を作る生成工程が高速化し、その成果を Lean へ変換することで検証工程も人間の逐語的確認から分離できる。
\[
\text{大量並列探索}
\rightarrow
\text{証明候補}
\rightarrow
\text{形式化}
\rightarrow
\text{機械検証済み証明}
\]
生成と検証の両方がこの速度で処理されると、「正しい証明を得るまで」が研究全体の唯一の律速段階ではなくなる。形式体系が受理した巨大な証明が次々に蓄積すれば、次に必要になるのは、その証明がなぜ成立するのか、どこに新しい考え方があり、既存の数学へ何を追加したのかを人間が理解する工程である。
6. 機械検証が終わっても数学的理解は続く
形式検証が与える保証は強い。形式化された命題が、採用された公理、定義、既証明定理から正しく導かれているかを、機械が一貫した規則で検査できる。有限個の入力に対して期待どおりの出力が得られることを確認するテストとは異なり、形式証明では命題そのものの論理的導出を検査対象にできる。
ただし、この保証が確定するのは「その命題が形式体系の中で正しく証明されたか」という点である。1,300 万行の Lean がすべてカーネルに受理されたとしても、その事実だけから、証明の中心的な考え方、再利用可能な補題、従来理論との関係、人間向けに説明するときの最小構造まで自動的に得られるわけではない。
ここで、機械検証と数学的理解の完了条件を分けて考える必要がある。
| 状態 | 完了条件 | 得られるもの |
|---|---|---|
| 形式検証済み | 証明項が定義、公理、既証明定理の下で要求された命題を導出している。 | 形式体系の内部で正しさが確認された証明が得られる。 |
| 構造理解済み | 証明を成立させる主要な補題、依存関係、論理的な分岐を説明できる。 | 証明全体を人間が追跡できる構造へ圧縮できる。 |
| 概念理解済み | なぜその構成が成立するのかを、再利用可能な概念や方法として説明できる。 | 別の問題へ応用できる数学的な見方や技法が得られる。 |
| 体系化済み | 既存理論との関係、適用範囲、一般化可能な部分、派生する問題が整理されている。 | 数学共同体が参照し、再利用し、教育できる知識として定着する。 |
この違いは、巨大な形式証明ほど大きくなる。たとえば 30,000 個規模の中間定理を含む証明がすべて正しいと機械的に確認できたとしても、その 30,000 個を同じ重要度で人間が理解する必要はない。むしろ必要なのは、どの補題が証明全体を支える中心部分で、どの補題が局所的な技術処理で、どの構成が別の問題にも適用できるのかを選別することである。
形式証明は完全性を優先して情報を保持する。人間の理解は、その完全な情報から意味のある構造を抽出する。前者では一つの抜けも許されないが、後者では大量の詳細を圧縮し、少数の概念で全体を説明できることに価値がある。この違いによって、同じ証明に対して機械と人間が扱う情報量の性質が変わる。
この区別は Clay Mathematics Institute の反応にも現れている。CMI は 2026 年 9 月 11 日、Navier–Stokes 問題について「apparently been settled」と述べた。そのうえで、解決の背後にある革新が分析され、検討されることで、新しい人間の理解が生まれることへの期待を表明している[15]。
CMI の反応には、同じ成果に対する二つの時間軸が含まれている。一つは、公式問題で要求された条件を満たす証明が提示され、数学的な決着へ近づく時間である。もう一つは、その証明が読み解かれ、新しい概念や方法として整理され、数学共同体へ吸収される時間である。前者が短時間で進んでも、後者まで同じ速度で進むとは限らない。
ここで律速段階が再び移動する。証明候補を作る工程が AI によって高速化され、証明の正しさを確認する工程が形式検証によって高速化されると、残る制約は「正しい証明から何を読み取るか」という工程になる。
\[
\text{生成済み}
\rightarrow
\text{検証済み}
\rightarrow
\text{理解済み}
\rightarrow
\text{体系化済み}
\]
この列の後半では、処理対象そのものが変わる。生成工程では候補を作り、検証工程では論理的妥当性を判定する。理解工程では、証明全体から意味のある構造を選び、圧縮し、説明可能な形へ変換する。体系化では、その構造を既存の数学へ接続し、他の問題でも再利用できる位置へ置く。
AI が数学研究の前半を高速化するほど、後半に残るこの圧縮と解釈の価値が大きくなる。正しい証明が希少だった時代には、証明へ到達すること自体が大きな成果だった。正しい証明を大量に生成し、機械的に検証できるようになると、その中から何を数学として理解し、何を知識として残すかという仕事が次の制約になる。
7. 未解決問題には理解を作る役割もある
前章までに見たように、AI が証明候補を生成し、形式証明系がその正しさを検証できるようになると、「問題を解く」という工程そのものは大幅に高速化できる。しかし数学における未解決問題は、解答を得るためだけに存在してきたわけではない。問題へ取り組む過程そのものが、新しい概念、補題、証明技法、分野間の接続を生み出す役割を持っている。
この点を明示的に問題提起したのが、2026 年 9 月 11 日に公開された声明「A Severe Misalignment of AI in Mathematics」である。25 人のフィールズ賞受賞者が初期署名者となり、AI 企業が未解決問題をモデル能力の評価対象として大量に解く方向と、数学共同体が数学を発展させる目的との間にずれが生じていると主張した[16]。Terence Tao も初期署名者の一人であり、自身のブログで声明の背景と問題意識を説明している[17]。
この声明が問題にしているのは、AI が正しい答えを出すことそのものではなく、未解決問題が数学の中で果たしてきた役割である。数学者は難しい問題へ取り組む過程で、既存の表現では捉えにくかった構造に名前を付け、必要な補題を作り、既存理論の不足部分を見つけ、別分野との関係を発見する。最終的に得られる定理は、その長い探索過程で形成された理解を圧縮した成果の一つとして位置付けられる。
たとえば、ある予想が真であることを証明するという目的だけを考えれば、必要なのは最終的な証明である。しかし研究過程では、その証明に到達するために導入された新しい概念が別の問題にも使われたり、途中で得られた補題が独立した研究対象になったりする。問題を解く過程が、その問題を超えて再利用できる数学を生み出す。
このため、未解決問題には少なくとも 4 つの役割を分けて考えられる。
| 役割 | 得られる成果 | AI による高速化との関係 |
|---|---|---|
| 問題の決着 | 命題の証明、反例、最適値などが確定する。 | 大規模探索と形式検証によって処理時間を短縮しやすい。 |
| 概念形成 | 新しい定義、見方、補題、証明技法が生まれる。 | 生成物の中から、どの構造が再利用可能な概念なのかを抽出する工程が必要になる。 |
| 知識統合 | 既存理論との関係が整理され、別の問題へ再利用できる。 | 成果数が増えるほど、どの成果を既存体系へ組み込むかという選別と整理の負荷が増える。 |
| 教育と継承 | 後続の研究者が内容を理解し、さらに発展させられる。 | 巨大な形式証明を、人間が扱える説明や概念へ圧縮する能力の価値が高まる。 |
AI による高速化が最も直接的に作用するのは、最初の「問題の決着」である。大量の探索を並列に実行し、得られた証明候補を形式検証へ渡せれば、命題の真偽を確定するまでの時間は短縮できる。前章までに見た Navier–Stokes やフェルマーの最終定理の形式化は、この前半工程が機械化されつつあることを示している。
一方で、概念形成や知識統合は、最終的な証明が得られた後にも続く。どの補題がその問題固有の技術なのか、どの考え方が別の分野でも通用するのか、既存理論のどこを書き換える必要があるのかを判断するには、証明全体を意味のある構造へ分解する必要がある。成果物の数が増えれば、この選別対象も増える。
ここで、未解決問題を「答えを得るための課題」とだけ見る場合と、「理解を形成するための研究装置」と見る場合で、AI による高速化の評価が変わる。前者では、短時間で多くの問題を解けること自体が直接的な進歩になる。後者では、解決数が増えるほど、その過程から得られた概念や方法をどこまで人間の数学へ変換できたかという別の評価軸が必要になる。
フィールズ賞受賞者の声明が指摘しているずれは、この二つの評価軸の差として読める。AI 企業にとって未解決問題は、既知のベンチマークより難しく、モデル能力を示す明確な成果になりやすい。一方、数学共同体にとって未解決問題は、研究者が長期間取り組むことで新しい数学を生み出す場でもある。同じ問題を扱っていても、何を成果として数えるかが異なる。
生成速度が上がるほど、命題の決着数を測定することは容易になる。何問を解いたか、どれだけ短時間で解いたか、形式検証まで完了したかという指標は数値化しやすい。しかし数学共同体が蓄積してきたものには、定理の一覧だけでなく、それらを理解するための概念体系、証明技法、分野間の関係、教育可能な説明も含まれている。
この違いを踏まえると、AI が未解決問題を大量に解くことによって直ちに数学的理解が失われると結論する必要はない。むしろ、問題の決着が高速化した結果として、どの成果から理解を抽出し、どの成果を人間の数学へ残すかという後続工程の重要性が増す。次に問われるのは、大量に生成された数学を人間がどのように選び、理解するかである。
8. 大量の数学が生まれること自体は理解の減少を意味しない
前章の声明は、未解決問題を大量に解くことによって、問題解決と概念的理解の結び付きが弱まる可能性を指摘していた。しかし、証明の供給量が増えることと、人間が得られる数学的理解が減ることの間には、もう一段の因果関係が必要である。大量生成された成果の中から重要なものを選び、理解し、既存理論へ統合できれば、人間が利用できる数学の量はむしろ増える可能性がある。
この立場から声明への署名を見送ったのが、フィールズ賞受賞者 Timothy Gowers である。Gowers は 2026 年 9 月 17 日にその理由を詳しく説明し、数学における問題解決と概念的理解の関係について、声明とは異なる見方を示した[18]。AI による変化そのものを否定するのではなく、大量の数学的成果が生成される状況を前提に、人間がその成果とどう関わるかを考える立場である。
この議論には以前からの背景がある。Gowers は 2000 年の「The Two Cultures of Mathematics」で、数学者の活動には、具体的な問題の解決を中心に進む文化と、一般的な理論や概念の構築を中心に進む文化があると論じた[19]。実際の数学研究では両者が分離して存在するわけではなく、問題を解く過程から理論が形成され、理論が整備されることで新しい問題が解けるという循環がある。
AI が大きく変えるのは、この循環のうち問題解決側の供給能力である。証明候補を大量に生成し、形式検証まで高速化できれば、従来より多くの解決済み問題が短期間に生まれる。一方、理論構築側では、それらの成果から共通構造を見つけ、一般化し、別の問題にも使える概念へ変換する必要がある。前者の処理能力が急増すると、両者をつなぐ選別と抽象化の工程が相対的に大きな役割を持つ。
| 段階 | 成果量が少ない場合 | AI によって成果量が増えた場合 |
|---|---|---|
| 問題解決 | 一つの成果を得るまでの探索時間が大きな制約になる。 | 大量並列探索によって、短期間に複数の成果を生成できる。 |
| 検証 | 数学者が個々の証明を読み、妥当性を確認できる。 | 形式証明系によって、生成量と人間の逐語的な確認量を分離できる。 |
| 選別 | 得られる成果が少ないため、多くの成果を個別に検討できる。 | どの成果が重要で、どの成果に人間の理解を投入する価値があるかを判断する必要が増す。 |
| 理解と体系化 | 個々の成果を時間をかけて既存理論へ取り込める。 | 多数の成果から共通概念を抽出し、人間が利用できる量へ圧縮する能力が必要になる。 |
この構造は、現在の学術研究にもすでに存在する。世界で公開されるすべての数学論文を、一人の数学者が読むことは前提になっていない。専門分野ごとに成果が選別され、研究者による再検証や引用を経て、重要な結果が概説論文、講義、教科書、標準的な定理へ取り込まれる。数学共同体は、すべての成果をすべての研究者が理解する方式ではなく、分業と選別によって知識量の増加を処理してきた。
AI による大量生成は、この既存構造の入力側をさらに拡大する。たとえば 1 年に数件しか得られなかった種類の成果が数百件得られるようになった場合、人間が数百件すべてへ同じ時間を配分する必要はない。重要な 10 件を選び、その証明から新しい概念を抽出できれば、人間が理解する重要数学の絶対量が従来より増える可能性がある。
ここで新しい希少資源になるのが選別能力である。形式検証によって正しい証明だけを抽出できても、「正しい」と「重要」は別の評価軸である。既存理論を大きく単純化する成果、複数分野を接続する成果、新しい証明技法を含む成果と、特定の条件下でだけ成立する局所的な結果では、人間が理解へ投入する時間の価値が異なる。
選別の次には圧縮が必要になる。数百万行の形式証明をそのまま人間の知識として保持する代わりに、その証明を成立させている数個の主要概念や補題へ整理する。さらに、複数の AI 生成成果に同じ構造が繰り返し現れるなら、それらを一つの一般理論としてまとめることができる。大量生成によって個別成果が増えるほど、それらを少数の概念へまとめる仕事の効果も大きくなる。
この観点では、AI による数学の大量生成と人間の数学的理解は、必ずしも反比例しない。両者の間には、検証、選別、圧縮、体系化という変換工程がある。その工程が機能すれば、AI が生成する数学の量を、人間が理解できる数学の増加へ変換できる。
一方、この変換能力より生成速度の方が大きくなれば、検証済みでありながら十分に理解されていない成果が蓄積する。前章で扱った懸念と Gowers の見方の差は、AI による大量生成そのものより、この変換工程をどこまで成立させられると考えるかにある。
そのため、AI 時代の数学で問われるのは、生成量を人間の読解量へ合わせることだけではない。増加した成果から、理解する価値の高いものを選び、短い説明へ圧縮し、再利用可能な概念を抽出し、既存の数学へ位置付ける能力が必要になる。大量の数学を生産する能力と、その中から数学として残すものを決める能力が分かれたとき、後者が人間の理解へ変換する入口になる。
9. 数学の進歩は証明の本数だけでは測れない
数学的理解を重視する考え方は、AI の登場によって突然生まれたものではない。William Thurston は 1994 年の「On proof and progress in mathematics」で、数学の進歩を定理や証明の蓄積だけで捉える見方を批判し、数学者が概念を理解し、それを他者へ伝達できる状態を作ること自体を数学の重要な活動として論じた[20]。
この見方では、一つの定理が証明された時点は知識形成の終点ではなく、その後に複数の変換工程が続く。最初の証明から主要な補題が切り出され、証明に使われた構造へ名前が与えられ、より短い別証明が見つかり、特殊な条件が一般化される。さらに、研究者向けの論文から概説、講義、教科書へと表現が変わることで、個別の成果が数学共同体で再利用可能な知識へ変わっていく。
| 段階 | 成果の形 | 数学共同体に加わるもの |
|---|---|---|
| 最初の証明 | 特定の命題を成立させる論理的な導出が得られる。 | 問題の真偽や成立条件が確定する。 |
| 構造の抽出 | 主要補題、証明技法、不変量、構成法などが切り出される。 | 個別問題を超えて再利用できる方法が得られる。 |
| 一般化 | 条件を緩めた定理や、より広い対象を扱う理論へ拡張される。 | 複数の個別成果を統一して説明する枠組みが形成される。 |
| 知識化 | 概説、講義、教科書など、人間が学習しやすい表現へ整理される。 | 後続の研究者が元の探索過程を再現せずに成果を利用できる。 |
この変換は、単なる文章の短縮ではなく、数学的情報の圧縮である。巨大な証明には、論理的に必要な細部が大量に含まれる。しかし後続の研究者が同じ成果を利用するとき、毎回その全細部を保持する必要はない。「この条件ではこの量が保存される」「この構成を使うと特異点が生じる」「この補題によって局所的な問題を大域的な問題へ移せる」といった少数の概念へ圧縮できれば、その概念を使って次の研究を開始できる。
圧縮によって失われるのは、再利用に不要な細部であり、残されるのは次の推論に使える構造である。元の証明が数百ページあっても、その成果が数個の定義や定理として教科書へ定着すれば、後続の研究者は元の論文を毎回読み直さずに、その成果を前提としてさらに先へ進める。数学が世代を超えて累積できる理由の一つは、この圧縮と再利用が繰り返されてきたことにある。
形式証明が巨大化すると、この役割分担がさらに明確になる。形式証明系は、論理的な抜けを許さず、定義から最終結論まで必要な情報を保持する。機械検証のためには、この完全性が価値になる。一方、人間が数学を理解するときには、数百万行の導出をそのまま保持するより、証明を成立させている数個の主要な構造を把握する方が有用である。
このため、機械向けの証明と人間向けの数学は、同じ内容を異なる粒度で保持することになる。形式証明は「すべての論理的ステップが成立していること」を保存し、人間向けの説明は「どの考え方によって全体が成立しているか」を保存する。前者は検証可能性を高め、後者は理解と再利用を容易にする。
AI が巨大な形式証明を大量に生成するようになると、この二つの表現の間を変換する仕事が大きくなる。証明が 1 件しかなければ、数学者はその成果へ時間をかけて主要概念を抽出できる。数百件、数千件の検証済み証明が短期間に供給されれば、どの成果から概念を抽出し、どの証明を一般化し、どの結果を教科書的知識へ昇格させるかという選別が必要になる。
ここで、証明の本数と数学の進歩を同一の尺度で測ることが難しくなる。AI が 1,000 件の新しい定理を証明しても、それらが互いに近い局所的な結果であれば、数学全体の理解が 1,000 倍増えたとは言えない。一方、一つの証明から新しい概念が生まれ、その概念によって多数の既存結果を統一的に説明できるようになれば、成果の本数以上に大きな変化が生じる。
つまり、数学の進歩には量と構造という異なる尺度がある。定理や証明の数は成果量を示すが、それらの間にどのような関係が見つかり、どの程度少ない概念で多くの現象を説明できるようになったかは、別の尺度である。AI が前者を急速に増やすほど、後者を形成する仕事の価値が相対的に大きくなる。
この観点から見ると、AI 時代の数学で希少になる理解とは、単に証明文を読めることを意味しない。大量の正しい成果から共通構造を見つけ、それを少数の概念へ圧縮し、既存理論へ位置付け、次の研究で使える形へ変換する能力を指す。形式証明が数学的情報を完全な形で保存するほど、人間側には、その完全な情報から何を残せば数学として前へ進めるのかを判断する役割が強く求められる。
10. 数学共同体による受容にも時間が組み込まれている
数学では、証明候補が公開された瞬間と、その結果が共同体で確立した瞬間は別の段階として扱われる。証明を書いた本人や形式証明系が正しいと判断しただけで、その成果が直ちに標準的な数学知識へ組み込まれるわけではない。第三者が内容を読み、前提を確認し、別の観点から検討し、その成果を既存理論の中へ位置付ける時間が必要になる。
この時間差を制度として明示している例が、Clay Mathematics Institute のミレニアム懸賞問題である。CMI の規則では、提案された解決が適格な媒体で公表されていることに加え、公表から少なくとも 2 年が経過し、世界の数学共同体で一般的な受容を得ていることが、CMI が解決案を検討するための条件に含まれている[21]。
ここで要求されている 2 年という期間には、単なる待機期間以上の意味がある。新しい証明が公開されると、他の数学者が論証を確認し、補題や定義の使い方を検討し、既存結果との矛盾がないかを調べる。その過程で別証明が作られたり、証明の一部が簡略化されたり、当初想定していなかった条件依存性が見つかったりすることもある。時間を置くことで、最初の成果物そのものだけでなく、その成果が数学共同体の中でどの程度安定して再現、説明、利用できるかが見えてくる。
| 段階 | 成立する状態 | 必要になる時間 |
|---|---|---|
| 証明候補の生成 | 問題に対する解決案が得られる。 | AI による大量並列探索で短縮しやすい。 |
| 形式検証 | 定められた形式体系の中で論理的導出が成立する。 | 形式証明系によって機械的に処理できる。 |
| 第三者検討 | 他の数学者が前提、論証、既存理論との整合性を確認する。 | 人間による読解、再検討、比較に依存する。 |
| 共同体による受容 | 成果が広く理解され、標準的な数学知識として扱われる。 | 複数の研究者と研究活動を通じた時間が必要になる。 |
| 制度的認定 | 賞や公式な解決認定の条件を満たす。 | CMI では公表後少なくとも 2 年という条件が明示されている。 |
この制度は AI 時代より前に作られたが、現在の状況では別の意味を持ち始める。従来は、一つの難問について証明候補が生まれるまでに長い時間がかかることが多く、その後に共同体が検討する時間も同じ研究史の中へ自然に組み込まれていた。AI が証明候補を数日単位で生成できるようになると、前半だけが急速に短縮され、共同体が理解し受容する後半の時間との差が大きくなる。
OpenAI の Navier–Stokes 発表は、その時間差がすでに現れている事例である。OpenAI は解決案と Lean 形式化を公開し、CMI は 2026 年 9 月 11 日に問題が「apparently been settled」と評価できる段階へ進んだことを発表した[15]。一方で、功績の評価や賞の認定については、既存の規則に沿って時間をかけて扱う方針を示している。
ここでは、形式的な正しさと共同体による受容の間にさらに一段の工程がある。形式証明によって論理的妥当性を高速に確認できても、その成果の数学的な重要性、既存理論との関係、証明技法の新規性、誰の貢献として位置付けるかといった判断は、形式検証だけでは完了しない。数学共同体は、正しいかどうかに加えて、その成果をどの位置へ置くかを決める。
生成速度がさらに上がると、この差は量として蓄積する。たとえば AI が 1 年に数百件の検証済み未解決問題を供給しても、数学共同体が同じ期間に十分な第三者検討と体系化を行える件数が数十件なら、残りは受容待ちとして積み上がる。前章までに扱った「理解待ち」に加えて、「共同体による評価待ち」という状態が生まれる。
このとき、数学の処理待ちは一つの場所に集中しない。形式検証済みであっても理解が十分でない成果、理解されていても重要性の評価が定まっていない成果、重要性が認められていても既存理論への位置付けが固まっていない成果が、それぞれ別の段階に滞留する可能性がある。
AI による数学研究の高速化を考えるとき、生成から受容までを一つの時間として見る必要がある。証明を作る時間だけが数日へ短縮されても、数学として確立するまでの全工程が同じ速度になるわけではない。むしろ生成と形式検証が速くなるほど、人間による検討、理解、評価、体系化に必要な時間が、数学全体の新しい処理能力を決める。
11. 高速化すると自動化しにくい工程が新しいボトルネックになる
ここまで見てきた構造は、数学固有の現象ではない。複数工程からなる知的生産では、一部の工程だけを高速化すると、その直後にある工程へ処理待ちが移る。OpenAI は自社の研究組織における AI エージェント利用を分析し、コード作成や実験実行が高速化しても、研究全体には仮説設定、実験設計、結果解釈、優先順位付けなど複数の工程が残るため、全体速度が同じ倍率で上がるわけではないと報告している。さらに、自動化が進むほど、自動化しにくい仕事が研究者の時間に占める割合を増し、次のボトルネックになると述べている[22]。
この現象は、ある工程の処理時間が短縮された結果として起こる。たとえばコード生成に 10 時間、実験実行に 10 時間、結果解釈に 10 時間かかっていた研究で、AI によって最初の 2 工程がそれぞれ 1 時間になったとする。全体時間は 30 時間から 12 時間へ短縮されるが、結果解釈の 10 時間は残る。その結果、以前は全体の 3 分の 1 だった解釈工程が、全体時間の大部分を占めるようになる。
数学研究でも、同じ律速段階の移動を考えられる。
\[
\text{問題探索}
\rightarrow
\text{証明生成}
\rightarrow
\text{形式検証}
\rightarrow
\text{選別}
\rightarrow
\text{理解}
\rightarrow
\text{体系化}
\]
従来は、問題探索と証明生成に長い時間を要することが多かった。証明候補が得られなければ、その後の検証も理解も始まらないため、研究速度は前半工程によって制約されていた。AI による大量並列探索によって証明生成が高速化し、さらに Lean のような形式証明系によって検証まで高速化すると、前半工程で発生していた待ち時間が縮小する。
| 工程 | 従来の主な制約 | AI による高速化後に残る課題 |
|---|---|---|
| 問題探索 | 有望な研究課題や証明方針を人間が長時間かけて探す。 | 多数の候補から、研究価値の高い問題を選ぶ必要がある。 |
| 証明生成 | 一つの証明候補へ到達するまでに長い試行錯誤を要する。 | 大量に生成された候補を後続工程へ渡すための選別が必要になる。 |
| 形式検証 | 人間が証明の各段階を読んで妥当性を確認する。 | 形式化された命題そのものが適切かを確認する必要が残る。 |
| 選別 | 成果数が少ないため、多くを個別に検討できる。 | 多数の正しい成果から、理解へ時間を投入する価値の高いものを選ぶ必要がある。 |
| 理解 | 証明を読み、主要な考え方を抽出する。 | 巨大な形式証明から人間が扱える少数の概念へ圧縮する必要がある。 |
| 体系化 | 個々の成果を既存理論へ徐々に組み込む。 | 大量の成果を整理し、重複、一般化、依存関係を管理する必要がある。 |
前半工程が高速化すると、後半工程の絶対的な処理能力が変わっていなくても、その存在が目立つようになる。証明候補が 1 年に数件しか得られなければ、数学者は一件ずつ時間をかけて読み込める。AI が同じ期間に数百件を生成し、形式検証まで完了させるようになれば、どの成果を読むかを決める選別工程が研究全体の処理量を制約する。
さらに AI が人間向けの解説まで生成できるようになっても、律速段階は消えない可能性がある。解説文そのものを作る速度が上がれば、次には「その解説が証明の本質を適切に捉えているか」「どの概念を重要と評価したか」「どの一般化に研究価値があるか」を判断する工程が残る。生成対象が証明から説明へ移っても、出力を評価し採用する工程が必要になる。
この構造では、自動化の対象が増えるほど、人間に残る仕事は単純に減るというより構成が変わる。機械が大量に処理できる工程から、人間による判断が必要な工程へ時間配分が移る。数学では、証明を作る能力の希少性が下がれば、成果の重要性を判断し、概念を抽出し、既存理論へ位置付ける能力の希少性が上がる。
ボトルネックは一度だけ移動するとは限らない。証明生成が高速化すれば検証へ移り、形式検証が高速化すれば理解へ移り、説明生成まで高速化すれば評価や体系化へ移る。技術が一つの制約を解消するたびに、その後ろに隠れていた次の制約が全体速度を決め始める。
この連鎖を考えると、AI による数学研究の進歩を「どこまで自動化できたか」だけで測ると不十分になる。より重要なのは、現在どの工程に処理待ちが発生しているか、そこへどの程度の人間の判断時間が必要かを見ることである。生成と検証が高速化した段階では、選別、理解、体系化が次の処理能力を決める。
12. 数学の希少資源は答えから理解へ移る
ここまでの事例を工程として並べると、数学研究のどこに処理能力が追加されているのかが見えてくる。Navier–Stokes の事例では、約 1 万の並列エージェントが探索を行い、約 88 時間で解決案へ到達した。その後、Lean への形式化と検証に追加で 17 時間を要した。フェルマーの最終定理では、Claude が 11 日間で約 1,300 万行の Lean を生成し、30,000 個規模の中間定理を含む機械検証可能な証明を構築した。どちらも、従来は人間の時間によって制約されていた生成と検証という前半工程へ、大きな計算能力を投入できることを示している。
この変化によって、数学研究全体が同じ倍率で高速化するとは限らない。証明候補を作る時間が短くなり、正しさを形式的に確認する時間も短くなれば、その後に残る成果の選別、数学的意味の理解、既存理論との接続、共同体による受容に必要な時間が相対的に大きくなる。前半工程の高速化によって、これまで探索時間の背後に隠れていた後半工程が全体の処理能力を決め始める。
| 希少性が高かった工程 | AI・形式検証による変化 | 次に希少になる工程 |
|---|---|---|
| 有望な証明方針を見つける | 多数のエージェントによる並列探索で候補生成量を増やせる。 | 多数の候補から検証対象を選ぶ。 |
| 証明の正しさを一つずつ確認する | Lean などの形式証明系へ検証を移せる。 | 検証済み成果から重要なものを選ぶ。 |
| 正しい証明へ到達する | 生成と検証を連続した計算処理として実行できる。 | 証明の主要概念を抽出し、人間向けに圧縮する。 |
| 個別成果を得る | 短期間に複数の成果が供給される。 | 成果間の関係を整理し、既存理論へ体系化する。 |
この後半工程の存在は、今回の議論に登場した数学者や組織の反応にも表れている。Clay Mathematics Institute は Navier–Stokes の問題が決着したと見られる段階へ進んだことを認めながら、その成果を分析することで新しい人間の理解が生まれることへ期待を示した。フィールズ賞受賞者による声明は、未解決問題を解くことと概念的理解を形成することの関係を問題にした。Timothy Gowers は大量生成そのものを否定する立場を取らず、問題解決と理論構築という数学内部に以前から存在する異なる価値の置き方から、変化への適応を論じた。
これらの立場は、AI による数学研究を同じように評価しているわけではない。しかし共通しているのは、最終的な証明が出力された瞬間だけで数学活動の全工程を説明していない点である。証明が得られた後にも、その内容を理解し、重要性を評価し、既存の数学へ位置付け、後続の研究者が使える知識へ変える工程が存在する。
Scott Aaronson は 2026 年 9 月 15 日、AI による数学成果が短期間に相次いでいる状況を踏まえ、今後自身が定理を証明するとすれば、必要性だけでなく楽しみや教育という理由が大きくなるだろうという見方を示した[23]。これは数学研究全体の将来を確定する予測ではないが、これまで数学者自身が担っていた「答えへ到達する」という仕事の位置付けが変わり始めたことへの反応として読める。
希少資源の移動は、供給量と処理能力の関係から説明できる。正しい証明が年に一件しか得られないなら、その一件を得る能力そのものに大きな価値がある。正しい証明が短期間に数百件供給されるようになれば、すべての成果へ同じ時間を投入することは難しくなる。この場合、価値を持つのは、どの成果を優先して読むかを判断し、巨大な証明から主要な構造を抽出し、他の成果との関係を見つける能力である。
この移動を、前章までの工程に沿ってまとめると次のようになる。
\[
\boxed{
\text{生成能力}
\rightarrow
\text{検証能力}
\rightarrow
\text{選別・理解・体系化能力}
}
\]
矢印は、前の能力が不要になることを意味していない。生成能力が十分に供給されると検証能力が制約として現れ、検証まで高速化すると選別、理解、体系化が次の制約として現れるという、律速段階の移動を表している。技術によって一つの希少性が緩和されるたびに、その後ろで必要とされていた別の能力が前面に出る。
この観点から見ると、数学者の役割も「証明を作る仕事」から単純に消滅するのではなく、配分が変化する。AI が大量の証明を生成できるほど、人間側には、どの成果が数学的に重要かを判断し、その成果を理解可能な構造へ圧縮し、複数の結果を統一する概念を見つけ、次の研究者が利用できる知識へ変換する仕事が集まる。
ここで扱われる理解は、単に AI の出力を自然言語で要約することより広い。ある証明のどこに新しい数学があるのか、既存理論のどの部分を変更するのか、どこまで一般化できるのか、別の成果と同じ構造を持つのかを判断する必要がある。この判断によって、個別の正しい証明が数学体系の一部へ変わる。
答えが希少だった時代には、答えへ到達することが研究の大きな制約だった。生成と検証の供給能力が増える時代には、正しい答えを数学として消化する能力が制約になる。AI が数学にもたらしている変化は、正しい答えの数が増えることだけに表れるのではない。答えが豊富になることで、何を理解し、何を知識として残すかという判断の希少性が、それまでより明確に見えるようになる。
参考文献
- id774, フェルマーの最終定理の形式化で、AI が生成した証明を Lean がどう検証したか（2026-09-07）. https://blog.id774.net/entry/2026/09/07/5616/
- id774, AI がテストを通しても、「正しい」とは限らない（2026-09-01）. https://blog.id774.net/entry/2026/09/01/5534/
- id774, AI に仕事を任せるには、モデルの外側を設計する（2026-08-21）. https://blog.id774.net/entry/2026/08/21/5544/
- id774, AI による大規模開発では、未確定な状態を一件ずつ閉じる（2026-08-15）. https://blog.id774.net/entry/2026/08/15/5503/
- OpenAI, Solving (some) formal math olympiad problems（2022-02-02）. https://openai.com/index/formal-math/
- OpenAI, An OpenAI model has disproved a central conjecture in discrete geometry（2026-05-20）. https://openai.com/index/model-disproves-discrete-geometry-conjecture/
- OpenAI, Ten advances in mathematics and theoretical computer science（2026-08-01）. https://openai.com/index/ten-advances-in-mathematics/
- Anthropic, Learning more about Claude’s mathematical capabilities（2026-08-10）. https://www.anthropic.com/research/riemann-zeta
- OpenAI, On the Navier–Stokes Millennium Prize Problem（2026-09-08）. https://openai.com/index/navier-stokes-solution/
- OpenAI, Finite Time Blowup for Navier–Stokes（2026-09-08）. https://cdn.openai.com/pdf/32d9f210-8b73-45e0-91bc-82a30aef8a9a/navier-stokes.pdf
- Charles L. Fefferman, Existence and Smoothness of the Navier–Stokes Equation. https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf
- OpenAI, Finite time blowup for Navier–Stokes and Euler equations. https://github.com/openai/NavierStokesAndEuler
- Anthropic, Formalizing Fermat’s Last Theorem（2026-09-04）. https://www.anthropic.com/research/formalizing-fermats-last-theorem
- Jeremy Avigad, Leonardo de Moura, Soonho Kong, Sebastian Ullrich, Theorem Proving in Lean 4. https://lean-lang.org/theorem_proving_in_lean4/
- Clay Mathematics Institute, Navier-Stokes Announcement（2026-09-11）. https://www.claymath.org/news/navier-stokes-announcement/
- A Severe Misalignment of AI in Mathematics（2026-09-11）. https://mathandai.org/
- Terence Tao, A Severe Misalignment of AI in Mathematics（2026-09-11）. https://terrytao.wordpress.com/2026/09/11/a-severe-misalignment-of-ai-in-mathematics/
- Timothy Gowers, Why I didn’t sign the Fields medallists’ letter（2026-09-17）. https://terrytao.wordpress.com/2026/09/17/why-i-didnt-sign-the-fields-medallists-letter/
- W. T. Gowers, The Two Cultures of Mathematics（2000）. https://www.dpmms.cam.ac.uk/~wtg10/2cultures.pdf
- William P. Thurston, On proof and progress in mathematics（1994-04）. https://arxiv.org/abs/math/9404236
- Clay Mathematics Institute, Rules for the Millennium Prize Problems（2018-09-26）. https://www.claymath.org/millennium-problems/rules/
- OpenAI, Research acceleration: The view inside OpenAI（2026-09-06）. https://openai.com/index/research-acceleration-view-inside-openai/
- Scott Aaronson, The Age of Wonders and Terrors（2026-09-15）. https://scottaaronson.blog/?p=10062