2026年8月1日、OpenAI公式サイトにデモ動画も豪華な画像もない一本の発表が掲載された。同社の次世代主力モデルの内部版である「Astra」が、数学および理論計算機科学における10の難問を一挙に解決したというのだ。これらの問題の中には数十年間にわたり放置され、何世代もの数学者が挑んでは敗れ、チューリング賞受賞者すら阻まれた難問が含まれている。発表から24時間以内に、Hacker Newsには600件以上のコメントが殺到した。だが筆者が最も驚かされたのは、そのコストである。OpenAIによると、10問すべての推論コストの合計はわずか約2000ドルだという。
2000ドルという金額が意味するものは何か。数学の博士課程学生の1ヶ月の奨学金すら下回る額だ。これは、数学研究における試行錯誤のコストが「人年（person-years）」から「ドル」へと移行していることを意味している。 ただし、この数字は公開API価格に基づいて算定された推論費用に過ぎず、モデルの巨大な学習コストは含まれていない。また、Astraが成功に至るまでに何千回の失敗を重ねたのかも公表されていない。この2点については後述する。
図：OpenAI公式サイトがこれら10の進展のために公開したカバー画像。出典：openai.com
なぜ数学の証明はこれほど難解なのか
まず、今回解決された問題の重量感を見てみよう。10の問題は高次元幾何学、符号理論、群論、量子計算、暗号理論、グラフ理論に及ぶ。代表的な3例を挙げる。
「非sofic群は存在するか」——群論分野における中核的な未解決問題であり、存在することは広く信じられていたものの、20年以上誰も具体例を構成できなかった。「最近ベクトル問題（SVP）」の近似難易度——暗号学界が30〜40年にわたり注視してきたテーマであり、耐量子計算機時代の暗号方式の根幹に直結する。「多色ラムジー数」の下限——伝説的数学者ポール・エルデシュ（Paul Erdős）が残した183番の問題であり、彼は生涯で1000問以上の懸賞問題を提示した。
なぜこれらの問題はこれほど難しいのか。数学の証明は迷路の中で出口を探すようなものである。一歩一歩に完全な論理的根拠が必要であり、一歩でも間違えればそれまでの計算はすべて無に帰す。普通の試験なら模範解答が存在するが、数学の未解決問題には存在しない。出口がどこにあるのか、そもそも出口が存在するのかさえ誰も知らない。人類の数学者は直感、経験、そして幸運に頼り、一度に1つのルートしか探索できない。
さらに別の難しさもある。これらの難問は「最初の着想の方向性」で停滞する。論証の出発点が間違っていれば、どれほど精巧に組み上げても徒労に終わる。過去何世代もの数学者が何十年もかけてどれほどの誤った方向性を排除してきたか、計り知れないが、その背景には膨大な人年が費やされている。
AIはいかにして難問を解き明かしたのか
OpenAIのアプローチは一言で要約できる。モデル自身に数千・数万の「証明の草案」を生成させ、それをマシンによって1つずつ検証させたのだ。
ここで決定的な役割を果たしたのが「Lean」である。Leanは形式検証ツールであり、厳格で公明正大な試験官のように機能する。証明をLeanが理解できる形式に記述すれば、行ごとに論理をチェックし、正しければパス、間違いなら即却下する。感情や人情の入り込む余地はない。AIの学習時、Leanの検証を通過した論証には報酬が与えられ、モデルは「検証可能な正解を書く」スキルを習得した。過去2年間でAIの数学能力が急上昇したのは、この自動採点機が存在したからにほかならない。 数学は、正誤を完全かつ客観的に判定できる数少ない分野である。文章執筆やプログラミングでは難しくとも、数学なら可能なのだ。
10万体の分身が同時に迷路に飛び込む光景を想像してほしい。大半は壁に激突して行き止まりとなるが、ごく一部が出口に到達する。試験官は完走したルートのみを認定する。人間は一度に1つの道しか進めないが、AIは同時に1万のルートを試すことができる。これは次元の異なるスケールメリットである。
今回の具体例では、内部版Astraが膨大な候補論証を生成し、Leanが有効な論証を抽出した。続いて人間の研究者がその論証を論文形式に整理し、さらにモデルが各ステップを形式化して機械的な再検証を可能にした。OpenAIはモデル自身の思考プロセスのログも公開している。10問すべてが解明され、消費されたトークン費用は合計で約2000ドルであった。
なぜ一般のユーザーにとっても重要なのか
第一に、AIが「人間がかつて書いたことのない新しい解答」を初めて提示した点だ。OpenAIによると、これらの問題の主要成果は少なくとも10年間、実質的な進展がなかった。かつてAIがアピールした数学能力は、既知の定理の再現や数学オリンピック問題の解法が主であったが、今回は数十年にわたり放置された本物のオープン問題である。
第二に、数学はあらゆる技術の上流に位置している。最近ベクトル問題は耐量子暗号に関わり、球充填や符号理論は通信やストレージ技術を支えている。数学という地盤が一段進めば、その上に構築される技術も遅かれ早かれ前進する。
第三に、コスト曲線が根本から変化した点だ。数学者のテレンス・タオ（Terence Tao）氏は今年、「ビッグ・マシーン・マス（Big Math）」という概念を提唱した。人間がアイデアを提供し、AIが泥臭い計算作業を担うという考え方だ。2000ドルというコストは、かつてトップ研究チームしか実施できなかった大量の試行錯誤が、今や個人の研究者でも実行可能になったことを意味する。今年5月にOpenAIがAIを用いてエルデシュの単位距離予想を否定して以来、少なくとも5本の人間による論文がその方向性を引き継いで執筆されている。AIの産出物が人間研究の新たな出発点となりつつあるのだ。
一般の人々にとって最も直接的なメッセージは、「AIが人間の書いたことのない新定理を生み出せる」という事実が、AIが単なる「既知の情報の言い換え」から遠く離れつつあることを示している点だ。この能力は数学の世界にとどまらず、いずれエンジニアリングやソフトウェア開発へ波及し、最終的には私たちが日常使うスマートフォンやサービスへと還元されるだろう。
楽観派 vs 懐疑派：どちらの主張が妥当か
Hacker Newsの議論では、2つの陣営が激しく対立した。
| 立場 | コアとなる主張 |
|---|---|
| 楽観派 | 成果は本物であり完全検証可能。Leanによる形式化によりハルシネーションや捏造の余地は極小である。もし一人の学生がこれらの問題を数問でも解けば、将来のフィールズ賞候補と目されるレベルだ。これは1997年にディープ・ブルーがカスパロフを破った瞬間の数学版と言える。 |
| 懐疑派 | 「超巨大な探索空間 ＋ 自動検証」によるブルートフォース（力任せ）に過ぎず、新しい概念的思想を生み出していない可能性がある。OpenAIはプロンプトや失敗回数を公開していない。技術的進展がS字曲線を描くのか指数関数的曲線を描くのかは議論の余地があり、ロケットというより登山に近いかもしれない。このような発表にはマーケティング目的が含まれ、主張と証拠の間には非公開の細部が存在する。1976年にコンピュータが四色問題を検証した際も数学者に違和感を与えたが、学問の質的転換には至らなかった。 |
両派ともに一理ある。懐疑派による最も強力な指摘は、あるHNユーザーから寄せられた。「Leanは『正しく記述された命題』を証明できるだけであり、命題そのものが問題の本質を捉えているかは人間が検証しなければならない」という点だ。マシンは推論プロセスを検証するが、問題自体を深く理解しているかは保証しない。これに対する楽観派の反論は至ってシンプルだ。「四色問題の検証以降、それは定理であり続けており、過去50年間誰も覆せていない」。
結び
数学者コミュニティの反応は二分されている。「数学の暗黒の夜の始まりだ」と憂慮する長文を寄せる者もいれば、数学がより多くの人々へ開放される契機と捉える者もいる。OpenAIは珍しく数学界の『ライデン宣言』を引用し、議論の存在を認めた上で、証明データ、形式化コード、思考プロセスログの公開を選択した。この透明性は、AI企業としては極めて稀である。
AIが数学者を代替するか否かを予測することは本質ではない。確認できる事実は3つある。10の難問が実際に解決され、Leanによって検証可能であること、コストが2000ドル規模であること、そして議論が始まったばかりであることだ。筆者の立場は明白である。「証明が成立するか」はマシンとピアレビューに委ね、「AIが数学を真に理解しているか」は時間に委ねるべきだ。AIが「真に数学を理解しているか」は哲学的な問いであり、時間がその答えを示してくれるだろう。
参考リンク：
- OpenAI: Ten advances in mathematics
- HN 討論 (item?id=49157930)
