OpenAIが次世代モデル群の一つとして位置付ける非公開の社内モデル「Astra」が、数学と理論計算機科学の分野で少なくとも10年以上未解決だった10件の問題について新たな結果を示し、機械的に検証可能な証明を公開した。もっとも、各結果の学術的な妥当性については、今後の専門家による精査が必要となる。

SiliconANGLEなどが2日（現地時間）に報じたところによると、OpenAIは249ページの原稿に加え、モデルが生成した推論過程とLean 4ベースの証明ファイルをGitHubでApache 2.0ライセンスの下で公開した。

公開された証明リポジトリでは、「sorry」の件数が0と表示されている。OpenAIはこれについて、形式化された証明に未完のステップが残っていないことを意味すると説明している。

代表的な成果として挙げたのが、1999年にミハイル・グロモフがソフィック性の概念を提示して以来、未解決だった非ソフィック群の明示的構成問題だ。Astraはこの問題で結果を示したとしている。

また、1980年にアラン・コンヌが提起した剛性予想については反例を示し、同一のフォン・ノイマン代数を共有する、異なる無限個の性質（T）群を構成したと発表した。

このほか、エルハルトの体積予想の証明や、ポール・エルデシュの問題リストに含まれる3件の解決も主張している。これには、多色ラムゼー数に関する183番問題も含まれるという。

OpenAIによると、残る結果は高次元球充填、二進・球面符号、算術回路複雑性、量子並列反復、最近接ベクトル問題の困難性など、幅広い領域に及ぶ。最近接ベクトル問題は格子暗号とも関係が深い。さらに、極値グラフ理論でも反例を示し、エルデシュ問題を追加で2件解いたとしている。

ソフィック群は、有限の置換によって近似できる構造を持つ群を指す。これまで研究対象となった群はすべてソフィック群とされてきた一方、あらゆる群がソフィック群であるかどうかは未証明のままだ。Astraは、この通説に反する例を示したと位置付けている。

コンヌ予想を巡っても、特定の剛性群のクラスでは関連する代数的対象が元の群を一意に識別できるとされてきたのに対し、Astraは同じ「指紋」を共有する異なる群を無限に構成したと説明した。

今回の発表の中核にあるのは、Leanによる形式証明だ。Leanのカーネルは、証明がコンパイル可能かどうかを二値で判定する。このため、形式検証の段階では、モデルの主張そのものを無条件に信頼する必要はないというのがOpenAIの立場だ。

ただし、形式化された命題が元の未解決問題を正確に表しているか、また結果が数学的にどのような意味を持つのかについては、数学者による検証が欠かせない。OpenAIが示した10件の結果はいずれも査読を経ていない。

OpenAIは過去にも同様の論争を経験している。2025年には、当時科学部門バイスプレジデントだったケビン・ワイルが、GPT-5がエルデシュ問題10件を解いたと主張したが、エルデシュ問題データベースを運営するトーマス・ブルームはこれを「劇的な歪曲」と批判した。

当時のモデルは既存論文を見つけるにとどまっていたとされ、ケビン・ワイルは後に当該投稿を削除した。Google DeepMindのCEOであるDemis Hassabisも、この件を当惑すべき事例だと評していた。

もっとも、今回は受け止め方がやや異なるようだ。トーマス・ブルームはAstraの結果を「大きなニュース」と評価し、自ら検証を手伝ったというOpenAI内部モデルの5月のエルデシュ単位距離反例を上回る成果だと述べた。

Astraは現時点で一般公開されていない。OpenAIは、複数のエージェントが長時間にわたって協調し、複雑な作業を遂行するよう設計したモデル群だと説明している。研究科学者のノアム・ブラウンが主導してきたtest-time推論研究の延長線上にあるという。

ノアム・ブラウンはX（旧Twitter）への投稿で、今回の結果を「科学的推論における重要な前進」と評価した。論文形式への取りまとめは人間が担ったが、数学的な論証自体はAstraが生成したのがOpenAIの説明だ。

OpenAIは、10件の解法に要したコストについて、GPT-5.6 SolのAPI料金ベースで約2000ドル（約30万円）だったとしている。

サム・アルトマンは最近、ワシントンの政策担当者にAstraをデモした。OpenAIは、リリース時期や価格、GPT-6への適用有無については未定としている。

実際に提供する場合でも、連邦のAI安全審査を通過する必要があるという。OpenAIによれば、これはGPT-5.6の提供を遅らせた手続きと同じものだ。

一方、国際数学連合はライデン宣言を支持し、AI企業が「同意なく公開研究を利用し、査読を迂回し、証明と著者表示の完全性を脅かす」と警告している。

ソフトウェアエンジニアのフェルナンド・ボレッティは、人間の数学者がこれまで依拠してきた防御論理が通用しなくなる可能性があり、AIが数学研究の最前線を変える余地があると指摘した。

OpenAIの今回の発表は、単なる技術成果にとどまらない。AIが生み出した数学的結果を学界がどの基準で検証し、受け入れるのか。あわせて、著作権や研究倫理をどう整備するのかを巡る新たな議論を促している。