OpenAIの新モデルAstra、数学の難問10件を2000ドルで解明

こんにちは！AIフル装備 powered by みらいラボのモモです。

OpenAIが2026年8月1日、新モデル「Astra」の内部版が数学と理論計算機科学の未解決問題10件を解いたと発表しました。いずれも10年以上研究者を悩ませてきた難問で、8つの分野にまたがります。

AIが単純な作業を代行する段階から、人間の専門家も解けなかった問題に答えを出す段階へ移った出来事として、研究者の間で話題になっています。今回はその内容と、何が本当に変わったのかを整理します。

発表の中心はAstraそのものの性能よりも、証明の「検証のしやすさ」にあります。この視点は、AI研究の今後を見るうえでも重要な手がかりになります。

AIが自ら答えを発見しただけでなく、その正しさまで機械で確かめられる形で示した点が、今回の発表の大きな特徴です。まずは何が解かれたのかを具体的に見ていきます。

Astraが解いた10件の問題と、その全体像

今回発表された成果は、OpenAIが公開前の次世代モデル「Astra」を使い、数学と理論計算機科学の未解決問題に取り組んだ結果です。対象は代数・幾何・組合せ論など幅広い分野に及びます。

群論から符号理論まで、8分野10問を解決

最も注目されている成果の一つが、「非ソフィック群」と呼ばれる群を具体的に構成した点です。これは数学者グロモフが1999年に提起した問いに、初めて明確な答えを与えるものです。

「ソフィック性」とは、群の構造を有限の対称群でどこまで近似できるかを表す性質です。近似できない具体例が長年見つからなかったため、今回の構成は群論の基礎的な問いに決着をつけたことになります。

ほかにも、フォン・ノイマン環に関する「コンヌの剛性予想」を反証し、「エルハート予想」という体積に関する予想を証明しました。さらにエルデシュの未解決問題集から3件（多色ラムゼー数を扱う問題183を含む）を解いています。

多色ラムゼー数とは、点と点を複数の色の線でつなぐとき、必ず同じ色の三角形などが現れる最小の点の数を指します。色の数が増えるほど計算量が爆発的に増え、問題183も長年具体的な数値が確定していませんでした。

分野ごとの内訳、球充填と符号理論の具体例

高次元の球充填問題では、単位球をどれだけ密に並べられるかを示す上界を更新しました。理論上の目標値である「コーン・エルキース限界」に一歩近づく結果とされています。

符号理論の分野では、誤り訂正に使う二値符号が取り得る最大サイズについて、指数的に改善した限界を示しました。これは通信やデータ保存の効率を左右する基礎的な指標のひとつです。

計算コストは2000ドル、ただし全体の費用ではない

OpenAIによると、これら10問の解答を見つけるのに使ったトークン計算のコストは、Sol APIのレートで合計約2000ドルだったとされています。2026年8月10日午前時点の為替レート(1ドル=約158円)で換算すると、日本円でおよそ32万円に相当します。

ただしこの金額は推論コストだけを指しており、Astra自体の訓練費用やインフラ費用、論文をまとめた研究者の人件費、証明を形式化する作業は含まれていません。発見そのものの単価が下がったという話であり、研究全体が2000ドルで完結したわけではない点は注意が必要です。

比較として、こうした未解決問題に人間の研究者が取り組む場合、助成金や研究時間という形で数年単位のコストがかかることも珍しくありません。単純比較はできないものの、計算資源側の単価がここまで下がったこと自体が今回の話題性につながっています。

Google DeepMindの手法と比べて何が違うのか

AIによる数学研究はAstraが初めてではありません。Google DeepMindも同様の取り組みを重ねてきましたが、Astraの成果は狙いも規模も異なります。

AlphaProofとAlphaProof Nexusとの違い

DeepMindの「AlphaProof」は2024年、国際数学オリンピックで銀メダル相当の成績を出し、5問中3問(幾何以外)を解きました。2026年5月に発表された後継の「AlphaProof Nexus」は、エルデシュの未解決問題353件のうち9件を解き、OEIS予想492件のうち44件を証明しています。

一方でAstraは、既存の未解決問題そのものを新たに解決した件数こそ10件と少なめですが、いずれも数十年単位で手つかずだった難問という点で毛色が異なります。数を競うより、質の高い難問に絞って結果を出した形です。

2024年のIMOでAlphaProofが解いたのは幾何以外の5問中3問で、幾何の問題は対象外でした。翌年以降のモデルはこうした弱点を踏まえて改良が重ねられており、AlphaProof Nexusはその延長線上にある成果です。

エルデシュの問題集を解くという意味

エルデシュの未解決問題集は、数学者ポール・エルデシュが生涯に提起した数百件の未解決問題を、研究者コミュニティが数十年にわたり整理・更新してきたものです。1件でも解けば専門誌に取り上げられるほどの難度が揃っています。

AlphaProof Nexusが353件中9件を解いたのに対し、Astraは同じ問題集から3件を解決しました。件数では及ばないものの、多色ラムゼー数を扱う問題183のように、組合せ論の中でも特に手強いとされる問題を含んでいる点が注目されています。

AlphaEvolveとの違いは「解決」か「改善」か

DeepMindのもう一つの成果「AlphaEvolve」は、既知の未解決問題50件超に適用され、そのうち約2割で従来の最良解を改善しました。改善とは、既に分かっている上界や下界の数値をより良い値に更新することを指します。

代表例が有限体版カケヤ予想の証明です。Gemini Deep Thinkが論理の筋道を提案し、AlphaProofがその内容を形式的な証明へ落とし込むという、複数のAIが役割を分担する形で検証が進められました。

これに対しAstraが示した10件は、上界・下界の改善ではなく、問題そのものに白黒の結論を付けた「解決」です。従来との違いを整理すると、AI数学研究は「既存の記録を更新する」段階から「未解決問題に結論を出す」段階へ広がってきたと言えます。

3つの成果を並べると、Astraが「新規解決」に重心を置いている点がより明確になります。

主要なAI数学ソルバーの比較

モデル	開発元・発表時期	主な成果	検証方法
Astra	OpenAI・2026年8月	未解決問題10件を新規に解決	Lean4形式証明・sorry数0
AlphaProof Nexus	Google DeepMind・2026年5月	エルデシュ問題353件中9件を解決、OEIS予想492件中44件を証明	Lean形式証明
AlphaEvolve	Google DeepMind・2025年5月	未解決問題50件超に適用、約2割で既知の最良解を改善	自動評価器による数値検証

いずれもLean(証明支援システム)を軸にしている点は共通していますが、検証の厳密さと対象規模の設計思想が異なります。

現場の数学者の反応と検証コミュニティの動き

数学者コミュニティの中には、Lean形式化に慣れた研究者が今回の証明を独自に再検証する動きも出てきています。専門誌への投稿を待たず、GitHub上のリポジトリに直接検証結果を報告する例も見られます。

従来は論文が専門誌に載るまで内容を広く共有しづらい面がありましたが、形式証明を先に公開する進め方によって、査読前の段階から誰でも検証に参加できる仕組みに変わりつつあります。

一部の未解決問題には、解決者に懸賞金が用意されているものもあります。ただし今回解かれた10問について、賞金付きの問題が含まれていたかどうかは今回の発表では明らかにされていません。

証明はどう検証すればいいのか

今回の成果が注目される最大の理由は、結果そのものより「検証のしやすさ」にあります。

そもそも「証明の形式化」とは何か

数学の証明は通常、人間の言葉と数式で書かれ、正しいかどうかは他の数学者が読んで判断します。「形式化」とは、この証明をLeanのようなソフトウェアが理解できる厳密な記法に書き直す作業です。

形式化された証明は、コンピューターが1行ずつ論理的な飛躍がないかを機械的に検査できます。手間はかかりますが、一度形式化できれば人間の読み間違いによる見落としが原理的に無くなる点が利点です。

料理の手順書で例えると、通常の証明は「経験豊富な人が読んで理屈が通っていると判断する」レベルに近い確認です。形式化された証明は、材料と手順をすべて数値化し、機械が同じ結果を再現できるかまで確かめる、より厳密なレベルの確認だと言えます。

sorryカウント0という機械保証の意味

証明はLean4という証明支援システムで形式化され、GitHub上でApache 2.0ライセンスのもとに公開されています。Leanには「sorry」という、証明の穴(未完成部分)を示す予約語があり、これが1件も残っていないことが機械的に確認できます。

つまり10件すべての証明について、論理の一歩一歩が正しくつながっていることをコンピューターが自動でチェック済みだということです。人間の査読者が数か月かけて追う作業を、当日中に機械検証で終えられる点が従来と大きく違います。

検証にかかる時間の変化

数学の重要な証明は、査読と検証だけで1年近くかかることも珍しくありません。専門家の人数が限られる分野ほど、この期間はさらに延びる傾向があります。

今回のように機械検証を前提にすると、検証そのものは数時間から当日中で完了します。査読の役割が消えるわけではありませんが、最初の正しさの確認にかかる時間は大きく短縮されることになります。

例えば1994年に発表されたフェルマーの最終定理の証明では、当初の原稿に誤りが見つかり、修正版が受理されるまでさらに1年以上を要しました。機械検証を前提にしていれば、同種の見落としはその場で検出できた可能性があります。

誰でも検証に参加できる公開の狙い

OpenAIは249ページに及ぶ英語のマニュスクリプトと、証明ファイルの両方を同時に公開しました。数学者でなくても、Lean4の処理系を動かせば同じ検証を自分の手元で再現できます。

従来のピアレビューでは、査読者の専門分野や人数に検証の質が左右されがちでした。形式証明を最初から前提にすることで、検証の再現性という点では新しい基準を示したと言えます。

どこまでが本当で、何を注視すべきか

成果の大きさに比例して、専門家の評価にも肯定と留保の両方が出ています。

専門家の見立て、誇張と実力の両方

マンチェスター大学の数学者トーマス・ブルーム氏は、今回の成果を「大きなニュース」と評価し、2026年5月に話題になった単位距離予想の反例よりも重要だと述べています。一方で、AIが数学者に取って代わるという見方には否定的です。

批評家のゲアリー・マーカス氏は「印象的だが過大に宣伝されている」と指摘しています。問題の選び方にAI側が答えやすいものを選んだ可能性、OpenAIの研究者による支援の有無、外部の第三者による独立検証がまだ済んでいない点が、今後確認すべき論点として残っています。

ブルーム氏は、エルデシュが提起した問題を一覧にまとめて更新し続けているデータベース「Erdos Problems」の管理者でもあります。2026年8月時点で同データベースには1217件の問題があり、565件(46%)が解決済みとされています。

今回の10問のうちエルデシュ問題集分がこの1217件のどれに対応するのかは、現時点の報道だけでは全て特定できていません。データベース側の更新状況を追うことで、今後さらに詳しい対応関係が分かってくると見られます。

検証インフラを持つ産業への広がり

今回の件で重要なのは、AIが答えを出すコストがほぼゼロに近づき、代わりに「正しさをどう保証するか」が制約になったという整理です。半導体設計のように、もともと形式検証の基盤を持つ産業では、この構造が特に生きてきます。

実際、チップ設計を手がけるCadenceやSynopsysのような企業では、AIが出した設計案を低コストで自動検証できる仕組みが既にあります。暗号技術や安全性が問われるソフトウェア分野でも、同じ構造が今後広がっていく可能性があります。

国内の実務者が見ておきたい視点

日本国内でも、半導体設計や金融のリスクモデルのように、正しさの厳密な証明が重視される分野は少なくありません。今回の手法がそのまま使えるわけではありませんが、検証コストを下げるという発想自体は参考になりそうです。

形式検証の基盤づくりには専門知識と時間がかかるため、導入は一部の大企業や研究機関が先行すると見られます。中小規模の現場に広がるまでには、ツールの使いやすさや人材育成といった課題も残ります。

まとめ

OpenAIの新モデルAstraは、10年以上手つかずだった数学と理論計算機科学の未解決問題10件を解き、Lean4による機械検証済みの証明とともに公開しました。計算コストはおよそ2000ドル(2026年8月10日時点のレートで約32万円)とされています。

このニュースが重要なのは、解けた問題の数そのものよりも、検証のプロセスが当日中に完了する形式に変わった点です。Google DeepMindのAlphaProof NexusやAlphaEvolveと並べると、AI数学研究が記録の改善から未解決問題への結論付けへ広がっていることが見えてきます。

今後は、問題選定の透明性や、OpenAI以外の第三者による独立検証がどこまで進むかが注目点になります。同じ手法が暗号技術や安全性が問われる分野にどう広がるかも、追いかけておきたいところです。

私自身は、AIが「答えを出す」だけでなく「その答えが正しいと機械で確かめられる」ところまで一体で示した点に、今回の一番の意味があると感じています。数学者の仕事を奪う話ではなく、これまで時間がかかっていた検証の壁を先に低くした出来事として、今後の広がりを見ていきたいと思います。

参考サイトまとめ

• Ten advances in mathematics and theoretical computer science（OpenAI公式）https://openai.com/index/ten-advances-in-mathematics/
• Ten Advances in Mathematics and Theoretical Computer Science（OpenAI公式マニュスクリプトPDF）https://cdn.openai.com/pdf/ten-proofs-oai.pdf
• OpenAI announces its “next major model” Astra by dropping ten previously unsolved math solutions（the-decoder）https://the-decoder.com/openai-announces-its-next-major-model-astra-by-dropping-ten-previously-unsolved-math-solutions/
• OpenAI’s Astra Solved Decades-Old Math Problems For $2,000（Forbes）https://www.forbes.com/sites/jonmarkman/2026/08/03/openais-astra-solved-10-decades-old-math-problems-for-just-2000/
• OpenAI Astra model solves 10 open math problems for $2,000（Quartz）https://qz.com/openai-astra-model-math-problems-lean-proofs-080326