数学の世界を、巨大で終わりのない図書館だと想像してみてください。長い間、この図書館における最も賢いAI「学生」たちは、優れた**ソルバー（解法器）**のようでした。彼らは、よく書かれた特定の宿題を与えられ、その指示を読み、答えを見つけ出すことに関しては驚異的な能力を持っていました。高校の数学コンテストの問題を与えれば、彼らはしばしば人間の天才よりも速く解いてみせました。彼らは、完璧に舗装されたトラックを走るレーシングカーのようなものでした。速く、正確で、信頼できる存在です。

しかし、この論文の著者たちは、私たちは壁に突き当たっていると主張しています。これらのソルバーは、レースを完走することには長けていますが、レースを発明することはできません。彼らは図書館を探索し、数十年間そこに置かれているままの、埃をかぶった未解決の謎を見つけ出し、それを解くための全く新しい方法を編み出すことはできないのです。

この論文は、もはやより優れたレーシングカーを作るのではなく、**リサーチ・エージェント（研究エージェント）**を作り始めるべき時が来ていると示唆しています。これらは単に指示に従うだけの学生ではありません。未知の領域へと足を踏み入れ、道に迷い、奇妙なアイデアを試し、そして――もしかすると――何か新しいものを発見できるような、探検家なのです。

現状： 「ソルバー」の時代

現在、AIは既知の課題において圧倒的な成果を上げています。

• MiniF2Fベンチマーク: これは、超難関の高校数学テストのようなものです。2021年、AIの正答率は約30%でした。2025年7月までに、Seed-Proverと呼ばれるシステムは、99.6%（244問中243問）の正解率を叩き出しました。これは実質的に満点です。
• IMO（国際数学オリンピック）: これらは世界最高峰の高校生たちに向けられた最難関の問題です。2024年、AlphaProofというAIは「銀メダル」レベルのスコアを獲得しました。2025年7月までに、Seed-Proverは2025年のコンテストから6問中5問を解きました。

これは驚くべきことです！これは、AIが厳密で、機械による検証が可能な数学を行えることを証明しています。しかし、ここに落とし穴があります。これらはすべて、宇宙の数学の世界に答えが「既に存在する」問題なのです。AIは単に、既知の宝物へと続く道を見つけているに過ぎません。

問題点： 「リサーチ・ギャップ（研究の溝）」

論文は、実際の数学研究がいかに混沌としているかを指摘しています。それは多肢選択式のテストではありません。それは、まるで積み藁の中から針を探すような作業であり、しかも、まだその針がどのような形をしているのかさえ分かっていない状態なのです。

著者たちは、現在のAIシステムは「フロンティア研究（最前線の研究）」に関して根本的な限界があると考えています。

• 「再発見」の罠: AIが有名な未解決問題（Erdős Problemsリストにあるような、1,100を超える難解な数学の謎のコレクションの一つ）を解いたと主張するとき、多くの場合、AIは人間がすでに本の中に書き残した解法を単に見つけ出しただけで、AI自身はそれを知らなかっただけなのです。
• 「ハルシネーション（幻覚）」のリスク: もし答えを知らない問題についてAIに解法を求めると、AIはもっともらしく見えるものの、実際には無意味な証明を捏造してしまうことがあります。人間であれば「行き詰まった、新しいアイデアが必要だ」と言えるところを、AIはしばしば自信満々に崖に向かって突き進んでしまいます。

この論文は、現在のAIが、次の大きな定理を発見する「単独の数学者」として準備ができているという考えを明確に否定しています。彼らは、DeepSeek-ProverやAlphaProofのようなシステムは、まだ単なる「ソルバー」に過ぎないと述べています。彼らは、人間の助けなしには、リーマン予想やナビエ・ストークス方程式のような真に未解決の巨人を扱うことはできません。

ロードマップ： ソルバーからリサーチャーへ

では、どうすればレーシングカーを探検家に変えられるのでしょうか？著者たちは、乗り越えるべき5つの大きなハードルを提示しています。

1. データの砂漠
たった10ページのテキストだけを読んで小説の書き方を学ぼうとする状況を想像してください。それが形式的な数学における問題です。インターネット上には何十億もの通常のテキストが存在しますが、形式的な数学のコード（Leanと呼ばれるシステムにおけるもの）はわずか130万行程度しかありません。

• 解決策: AIに「人間の数学（曖昧で文脈に依存するもの）」を「コンピュータの数学（極めて精密なもの）」へと翻訳することを教える必要があります。これは**オートフォーマライゼーション（自動形式化）**と呼ばれます。論文は、これが改善されつつあるものの、依然として困難であると示唆しています。翻訳における小さなミスが、難しい問題を簡単に見せたり、簡単な問題を不可能に見せたりすることがあります。

2. 失われた地図
現在のAIは、あらゆる数学の問題を独立した島として扱っています。しかし、実際の数学では、すべてがつながっています。幾何学の証明は、代数学の補題に依存していることがあります。

• 解決策: 巨大な**知識グラフ（Knowledge Graph）**を構築する必要があります。すべての定理がノード（節）となり、それらを結ぶ線がどのように関連しているかを示すウェブを想像してください。もしAIがこれらのつながりを見ることができれば、毎回ゼロから始めるのではなく、古いアイデアを使って新しい問題を解くことができるようになります。

3. 検証から発見へ
現在、AIは証明が正しいかどうかをチェックすること（検証）には長けています。しかし、証明自体を生み出すこと（発見）は苦手です。

• 解決策: 新しい定理を**推測（コンジェクチャ）**し、それを証明しようとするシステムが必要です。AlphaEvolveのような実験では、自然界が種を進化させるように、AIにアイデアを「進化」させることでこれを行おうとしています。しかし、論文はこれはまだ初期段階にあり、AIはまだ人間の天才のように「新しい数学的概念（新しい種類の数など）」を自ら発明することはできないと指摘しています。

4. ツールベルト（道具箱）
人間の数学者は脳だけを使うのではありません。計算機、コンピュータ、ソフトウェアなどのツールを使い、重労働を行います。

• 解決策: AIもこれらのツールを使う術を学ぶ必要があります。しかし、ここには注意点があります。もしAIが計算機に計算を依頼した場合、その計算機が間違えていないことをどうやって保証するのでしょうか？論文は、AIが外部ツールの成果に騙されないよう、それらの作業をチェックするためのより良い方法が必要であると示唆しています。

5. 人間とAIのダンス
論文は、未来は「AI vs 人間」ではないと主張しています。それは**「AI + 人間」**です。

• 解決策: AIを超高速の「研究助手」と考えてください。AIは数千の論文を瞬時に読み、1,000通りの証明をチェックし、データを整理できます。人間は**キャプテン（船長）**であり、直感、いわゆる「勘」、そしてそのアイデアが本当に素晴らしいものなのか、あるいは単なるハルシネーション（幻覚）なのかを判断する最終的な審判を提供します。
• 現実世界の例: 2025年後半、Aristotleという名前のAIエージェントが、Erdősリストの問題の一つを解決する手助けをしました。それは証明を生成しましたが、結局のところ、それが解いたのは元の問題のわずかに「弱められた（簡略化された）」バージョンであることが判明しました。元の問題は依然として未解決であることを理解するために、人間の数学者が介入する必要があったのです。これは、AIが強力であっても、それを誠実なものに保つためには人間が必要であることを示しています。

結論

この論文は、行動への呼びかけです。こう言っています。「私たちは素晴らしいソルバーを構築してきました。彼らはどんな数学コンテストでも勝つことができます。しかし、人類の知識の境界を押し広げるためには、私たちはリサーチ・エージェントを構築しなければなりません。」

これらのエージェントは単にルールに従うだけでなく、新しいルールを書く手助けをするでしょう。しかし、論文は明確に述べています。私たちはまだそこには到達していません。現在のAIは、輝かしい見習いであって、マスター（達人）ではないのです。AIには、より良いデータ、より良い地図、より良いツール、そして何よりも、暗く未知の領域へと導くための人間のパートナーが必要です。

「解くこと（Solving）」から「発見すること（Discovering）」への旅は、次なる大きな飛躍であり、そこへ到達するにはチームの総力が必要となるでしょう。