OpenAIの未発表モデル「Astra」が、10個の未解決数学問題を2000ドルで解いた
8月1日、OpenAIが一風変わった発表を行った。まだ一般公開されていない次期主力モデル「Astra」が、数学と理論計算機科学の分野で10年以上未解決だった問題を10個解き、しかもその全てに「機械が検証できる証明書」を添えて公開したのだ。エンジニアとしてこのニュースが興味深いのは、成果そのものよりも「なぜ今回は信じられるのか」という部分にある。
「またAIが数学を解いた」への根強い不信感
このニュースを聞いて、既視感を覚えたエンジニアも多いはずだ。実は2025年10月にも、当時のOpenAI幹部が「GPT-5がエルデシュ予想の未解決問題を10個解いた」と発表したことがあった。しかしこの発表は数日で崩れ去った。数学者のトーマス・ブルーム氏が検証したところ、モデルは既存の文献から解法を「検索」していただけで、独自に証明を組み立てていたわけではなかったことが判明したのだ。
今回のAstraの発表が違うのは、当のブルーム氏自身が「これは重要なニュースだ」と評価している点である。彼を含む数学コミュニティを納得させた仕組みが、今回の発表の核心と言える。
証明を「読める」形ではなく「検証できる」形で出す
技術的なポイントは、Lean 4という「定理証明支援系」（数学的な証明を、プログラムのようにコンピュータが一行ずつ検証できる形式で記述するツール）を使って、10個すべての証明を形式化した点にある。
通常、AIが生成した数学の証明は、人間の数学者が読んで「正しそうだ」と判断するしかない。しかしLean形式の証明は、読者が自分のノートPCで実際にコードを走らせるだけで、証明が本当に正しいかどうかを機械的に確認できる。OpenAIが公開したリポジトリでは、証明の未完了箇所を示す「sorry」という予約語の出現数がゼロだと報告されている——つまり、全ての論理ステップに抜け漏れがない状態で完結しているということだ。
これは、AIの出力を「信じる」ことから「検証する」ことへとシフトさせる、実務上とても大きな違いだ。
目玉は27年間未解決だった群論の問題
10個の結果は、群論、フォン・ノイマン環、高次元幾何学、量子計算量、格子暗号、極値組合せ論と、幅広い分野にまたがっている。中でも目玉とされているのが、「非ソフィック群」と呼ばれる群の具体的な構成例を初めて示した結果だ。
これは、数学者ミハイル・グロモフ氏が1999年に「ソフィック性」という概念を提唱して以来、27年間にわたって誰も証明も反証もできなかった、群論における中心的な未解決問題だった。この問題が今回、初めて決着したことになる。
わずか2000ドルという計算コストの意味
OpenAIの研究責任者セバスチャン・ビュベック氏によれば、10個すべての解を導き出すのにかかった計算コストは、同社のAPI料金換算でおよそ2000ドルだったという。これは象徴的な数字だ。数十年単位で人類の頭脳を悩ませてきた問題が、コーヒー数百杯分程度のコストで解けてしまったことになる。
ただし、この数字を鵜呑みにする前に押さえておくべき点もある。これはあくまで「解を導出するのに使われたトークンの、リスト価格ベースでの費用」であり、そのモデルを訓練するために投じられた莫大な研究開発コストは含まれていない。
数学界からは「歓迎」と「慎重な期待」が同居
この結果は、単にAI企業の自己申告として消費されているわけではない。2026年6月には、テレンス・タオ氏やピーター・ショルツ氏、スコット・アーロンソン氏ら著名な数学者が名を連ねる「ライデン宣言」という文書が、国際数学連合の支持のもとで発表されていた。この宣言は、AIと数学の関わりにおけるリスクとして、結果の信頼性の低さ、出典の欠如、閉じた商用システムへの依存、誇張された主張、そして科学的独立性の喪失という5点を挙げている。
今回のAstraの発表は、この5つのリスクのうち少なくとも3つに正面から向き合う形で設計されている。証明はLean形式で検証可能であり、249ページに及ぶ技術文書と、モデルがどう推論を組み立てたかを説明する62ページの解説文書まで公開された。「結果だけ見せて信じてくれ」ではなく、「検証プロセスごと渡すので好きに疑ってくれ」というスタンスだ。
エンジニアとして見ておきたいこと
このニュースの本質は、「AIが数学を解けるようになった」という話ではない。「AIが出した結果を、第三者が独立に、しかも機械的に検証できる仕組みが整い始めた」という点にある。
生成AIの出力を実務に組み込む際、多くのエンジニアが直面するのは「この出力は本当に正しいのか、どうやって確認すればいいのか」という壁だ。今回のケースは数学という極めて検証しやすい領域での成功例だが、「AIの生成物に、検証可能な形式の裏付けをどう持たせるか」という発想は、コード生成や設計文書のレビューなど、より身近な開発現場にも応用されていく視点になりそうだ。
OpenAIは今後、10万人の学術研究者に2027年まで自社のフロンティアモデルへの無料アクセスを提供するとも発表している。研究インフラを自社プラットフォームに囲い込む動きとも取れるが、少なくとも「検証可能な証明」という文化が、AIと数学研究の関わり方の標準になっていくとすれば、それ自体は歓迎すべき方向性だろう。