8月1日、RuntimeWireが「OpenAI says unreleased Astra model solved 10 open math problems」と題した記事を公開した。AIが数学の未解決問題を「解いた」という主張はこれまでも存在したが、Astraの発表がそれらと一線を画すのは、スコアではなく249ページの論文草稿・推論ウォークスルー・Leanの形式証明コードという「検証可能な成果物」を外部に公開している点だ。
未公開モデルが未解決問題10件に挑む
OpenAIは8月1日、次期主力モデルとして開発中の「Astra」の内部版が、数学および理論計算機科学における長年の未解決問題10件で新たな結果を生み出したと発表した。
この発表が従来の競合モデルとの違いを際立たせているのは、ベンチマークスコアではなく、研究者が実際に検証できる成果物を伴っている点だ。OpenAIは249ページに及ぶ論文草稿集、推論の過程を示すウォークスルー、そしてLeanの証明コードを収めた公開GitHubリポジトリを合わせて公開した。
Leanは形式証明支援系と呼ばれるツールで、数学的な論証が前提から機械的に正しく導かれているかを自動検証できる。自然言語による証明よりも強力なチェック機構として機能する。
OpenAIの研究科学者であるNoam Brown（@polynoamial）はXへの投稿で、Astraを「科学的推論における大きな一歩」と表現した。Brown氏は推論・強化学習・自己対戦・マルチエージェントシステムを専門とし、以前はMeta FAIR研究所でゲーム「ディプロマシー」をプレイするAIシステムCICERO、カーネギーメロン大学ではポーカーAIシステムLibratus・Pluribusに携わっていた人物だ。
10件の成果が示す領域の広さ
今回Astraが結果を出したとされる10件の問題は以下の領域にわたる。
- 高次元球充填問題（元記事では長年進展がなかったとされる問題に対する改善を主張。ただし「1978年以来」という年号は元記事本文中に明示された根拠が確認できないため、本稿では留保する）
- 2値符号・球面符号
- 非ソフィック群の明示的構成（すべての可算群が有限置換で近似できるかという未解決問題に関連）
- Connesの剛性予想の否定証明
- 算術回路複雑性（計算の基本的限界に関わる）
- 量子並列反復
- 最近傍ベクトル問題（CVP）：格子理論および耐量子暗号の中核を成す問題
- Ehrhartの体積予想
- 多色ラムゼー数
- 極値グラフ理論の2つの予想
純粋数学にとどまらず、耐量子暗号や計算複雑性理論に直結する問題が含まれている点は、エンジニアとして見逃せない。
最も大きな主張のひとつが非ソフィック群の明示的構成だ。これはすべての可算群が有限置換群で近似できるか否か、という長年の未解決問題の解決に相当する。
もうひとつ注目されるのがConnesの剛性予想の否定証明だ。Connesの埋め込み予想とも関連するこの問題は、作用素環論（ヒルベルト空間上の作用素を代数的に扱う数学の分野）における基本的な未解決問題のひとつであり、量子情報理論とも接点を持つ。その否定的結論を形式証明付きで示したとする主張は、数学コミュニティでも高い注目を集めている。
推論コストは約2,000ドル — モデルとの関係について
OpenAIは、10件の解を得るために使用したトークン量が約2,000ドル相当に相当すると説明した。元記事ではこの換算にあたり「GPT-5.6 Sol APIの料金体系」が参照基準として用いられている。Astraは未公開モデルであり独自の料金体系を持たないため、OpenAIが現行APIの料金表を用いてトークンコストを外部向けに示したものと解釈するのが自然だ。AstraとGPT-5.6 Solが同一モデルであることを示す記述は元記事には見当たらない。
なおこの数字は推論トークンのコストのみを示したものであり、Astraの学習コストや、問題の選定・論文原稿の準備・出力の確認にかかった人的作業は含まれていない。
証明の生成フローと人間の役割
OpenAIの説明によれば、Astraが数学的論証を生成し、その後人間が同モデルを使いながら論文草稿として整形した。さらにAstra自身がLeanによる形式化も担当した。OpenAIは成果物の正確性について責任を負うとしつつ、根拠となる論証の生成をAstraの功績としている。
なお、Lean証明による機械的な検証が可能になったとはいえ、各形式的命題が元の未解決問題の意図を正確に捉えているか、前提条件が適切か、各分野における数学的重要性はどの程度かといった点は、依然として専門家による精査が必要だとOpenAI自身も認めている。
DeepMindとの競争と、OpenAIの戦略的な位置づけ
Google DeepMindも同じ方向を追っている。Gemini Deep Thinkプログラムでは、数学エージェント「Aletheia」が専門家の指導のもと解を生成・改訂する取り組みを進めており、以前は学生向け数学コンテストでゴールドメダルレベルの成績を記録している。DeepMindの関連研究についてはGoogle DeepMindの研究ページから参照できるが、AletheiaおよびGemini Deep Thinkに特化した公開ページは現時点では確認できていない。
Astraの発表はそれを上回る規模で、複数の分野にまたがる10件の提案を一度に示した点で競争水準を引き上げている。
OpenAIはこの方向への布石をすでに打っていた。5月には未公開モデルが80年来の幾何学の未解決問題「Erdős単位距離予想」の反例を生成したと開示している。Astraはその1件から複数分野への拡張であり、「次の主力モデルを研究インフラとして位置付ける」という製品戦略の具体化と言える。
ただし、Astra自体はまだ内部モデルであり、リリース日・料金・アクセス条件・モデルカードはいずれも公開されていない。今回の発表は、モデルのリリースではなく、外部の専門家が検証可能な成果物を添えた「能力プレビュー」として機能している。
詳細はOpenAI says unreleased Astra model solved 10 open math problemsを参照していただきたい。
