OpenAIが、まだ一般公開していない次期主力モデル「Astra」の社内版を使い、数学と理論計算機科学の未解決問題を10件解いたと明らかにしました。いずれも10年以上、誰にも決着をつけられなかった問題です。同社は249ページの原稿に加えて、結果ごとに機械が正しさを検査できるLean 4の証明をGitHubで公開しました。成果を主張するだけの発表とは、検証のしやすさという点で性格が異なります。

主張ではなく「コンパイルが通る証明」を出した

今回の発表でまず目を引くのは、10件すべてにLean 4の証明が添えられている点です。Leanは数学の証明を形式言語で記述し、その正しさを計算機に機械的に検査させるための処理系です。書かれた証明は通るか通らないかのどちらかで、途中の飛躍や曖昧な言い換えは受け付けません。

AIが出した証明には、専門家が読み解くのに時間がかかりすぎて独立検証が進まない、という批判が付いて回ってきました。Lean証明が付いていれば、モデルの出力そのものを信用しなくても、Leanコンパイラを持っている人なら誰でも手元で結果を確かめられます。数学界が繰り返し指摘してきた検証の問題に対して、形式で応じた格好です。

27年開いていた群論の問題に決着

10件のうち中心に据えられているのが、非ソフィック群の初めての明示的な構成です。ソフィック性という概念は1999年にMikhail Gromov氏が導入したもので、それに当てはまらない群が存在するのかどうかは、群論の中心的な問いとして27年にわたり未解決のままでした。存在を示すことも、存在しないと示すこともできた数学者はいませんでした。

残る9件は分野をまたいでいます。フォン・ノイマン環に関するConnesの剛性予想の反証、Ehrhartの体積予想の証明、Paul Erdős氏が残した問題集からの3問（多色ラムゼー数を扱う183番を含む）、1978年以来となる高次元球充填密度の一般上界の改善、2人プレイヤー量子ゲームの並列反復定理、そしてパーマネントを計算する回路計算量の新しい下界です。群論、作用素環論、高次元幾何、量子計算量、格子暗号、極値組合せ論と、守備範囲はかなり広く取られています。

10件合計の計算コストは約2,000ドル

OpenAIによると、10件すべてを解くのにかかった計算コストは、Sol APIの料金換算で合計およそ2,000ドル（約31万円）でした。同社の数学研究責任者であるSebastien Bubeck氏はXで結果を認め、beautiful（美しい）と評したうえで、各結果にLean証明と思考過程の解説が付いていると説明しています。

※1ドル156.5円換算（2026年8月3日時点）

数学界との距離感は微妙なまま

もっとも、この発表が置かれている状況は穏やかとは言えません。6月には数学者たちがライデン宣言を出し、国際数学連合もこれを支持しました。宣言は、AI企業が公開された研究成果を同意なく利用し、査読を迂回し、証明と帰属の健全性を脅かしていると警告する内容で、査読誌ではなくプレスリリースで結果を発表する企業のやり方を名指しで問題視しています。

OpenAIには前例もあります。5月には同じ長時間推論モデルの系列が、80年来の離散幾何の問題であるエルデシュの単位距離予想を反証したと発表しました。このときフィールズ賞受賞者のTim Gowers氏は、その証明をAnnals of Mathematicsに推薦することをためらわないと述べています。今回についても、erdosproblemsというサイトを運営するThomas Bloom氏がXで、単位距離の反例より重要な成果だとして注目すべきだと書きました。評価する声はあるものの、ブログ記事で発表された結果を数学界全体がどう受け止めるのかは、まだ答えが出ていません。

Astraの正体は明かされていない

肝心のAstraについて、OpenAIは公開時期を示しておらず、次の主要モデルとだけ説明しています。投資家のMark Kretschmann氏をはじめ、GPT-6系列ではないかと推測する声もありますが、確定した情報はありません。同社は2027年まで研究者10万人にフロンティアモデルへの無償アクセスを提供する取り組みも進めており、科学分野との結び付きを強める動きが続いています。

まとめ

未発表モデルが10年以上開いていた数学の問題を10件解き、しかもすべてに機械検証可能なLean 4の証明を添えた、というのが今回の要点です。計算コストは合計で約2,000ドルにとどまりました。検証手段が用意された点は前進ですが、査読を経ない発表の是非という論点は残ったままで、Astra自体の公開時期も不明です。数学の道具としてAIをどう扱うかという議論は、ここからさらに動きそうです。