OpenAIが数学の未解決問題10個を一気に解いた「Astra」の実力

LLMが数学の最先端に到達した

2026年8月1日、OpenAIが発表した 「Ten advances in mathematics and theoretical computer science」 は、AIの研究能力を世界中に見せつける出来事でした。未リリースの内部モデル「Astra」を使い、高次元幾何学、符号理論、量子計算量、格子暗号など10個の未解決問題で新たな成果を出しています。

解かれた10の問題

発表された成果は以下の10個。どれも各分野で長年議論されてきた難題です。

  • 高次元球充填 — Cohn–Elkies閾値までの新しい上界
  • バイナリ符号・球面符号 — 最小距離ごとの最大サイズの指数的改善
  • 非sofic群の存在 — 群論の中心的未解決問題に決着
  • Connesの剛性予想の反例 — フォン・ノイマン代数が群を一意に決定するという長年の予想を否定
  • 算術回路計算量 — 永久行列式のarithmetic formulaに対する n⁴/log n オーダーの下界
  • 量子並列反復定理 — 2プレイヤー量子ゲームに対する指数的並列反復定理
  • 最近接ベクトル問題(CVP) — ポスト量子暗号に関連する格子問題の多項式因子近似硬度
  • Ehrhartの体積予想 — 全次元での最大体積の決定
  • 多色ラムゼー数 — Erdős問題183の解決(超指数的下界)
  • 極値グラフ理論の予想 — compactness予想とdegeneracy予想、Erdős問題146・180の解決

コストは約2,000ドル

驚くべきはそのコストです。OpenAIによると、これら10個の問題を解くのに必要だったトークン量は、Sol API料金で約2,000ドル(約30万円)でした。天才数学者たちが何十年も取り組んできた問題を、たった30万円相当の計算で解いてしまったわけです。

もちろん、そこには人間の専門家の関与もあります。モデルが出力した証明を論文形式にまとめ、Lean(定理証明支援系)で形式化する作業は、人間とモデルの協力で行われました。Leanの証明証明書はGitHubで公開されています。

専門知識がさらに価値を持つ時代

Hacker Newsで同時に話題になっていたSean Goedeckeの記事 「LLMs reward expertise」 が、このニュースと非常に相性が良いです。

彼の主張はシンプル:「LLMを使いこなす最大のスキルは、その領域の専門知識だ」

例として挙げられているのは、数学者テレンス・タオとChatGPTの対話。タオは短く的確な質問で、モデルを「数学者向けモード」に切り替え、素人向けの長い説明を省かせています。同じChatGPTでも、専門家と素人とでは引き出せる価値が全く違う。

OpenAIの数学プロジェクトでも同じ構造があります。モデルが証明を生成しても、それが正しいかを判断し、どの方向に掘り進めるかを決めるのは人間の数学者です。AIが「出力」しても、専門家が「方向づけ」しなければ到達できません。

てっちゃん的視点 🔍

この件で重要なのは3点です。

  • AIは「解く道具」から「発見するパートナー」に進化した — MayのErdős予想の反例に続き、今回は10個同時。もはや偶然ではない
  • 専門知識の価値は下がらない、むしろ上がる — モデルが強くなるほど、それを正しい方向に導ける人材の価値が相対的に高まる
  • 検証可能な形での公開が重要 — Lean証明書の公開など、AI生成の成果をコミュニティが検証できる仕組みを作っている点は評価できる

まとめ

AIが数学の最先端に到達した2026年夏。モデル単体でも凄いですが、「専門家 × AI」の組み合わせこそが真の突破口だという事実を、てっちゃんのような技術者視点でも実感できるニュースでした。

「みんな同じLLMを使っている」時代に、差がつくのはドメイン知識です。LLMが出力して終わりではなく、それをどう方向づけるか。そこに人間の価値があります。


参考:OpenAI公式発表 / Lean証明書(GitHub) / LLMs reward expertise(Sean Goedecke)