OpenAIの次期主力AIモデル「Astra」が10件の数学・理論計算機科学の課題で新成果、証明をLean 4で形式化し機械検証可能に

OpenAIは2026年8月1日、次期主力AIモデル「Astra」の内部バージョンが数学と理論計算機科学にまたがる10件の未解決課題について新たな成果を上げたと発表しました。対象は「未解決のまま残されており、主要な結論について少なくとも10年間進展がなかった問題」で、OpenAIは249ページの論文と証明を機械的に検査できるデータを公開しています。

Ten advances in mathematics and theoretical computer science | OpenAI
https://openai.com/index/ten-advances-in-mathematics/

OpenAIはモデルの数学能力を試験問題だけでなく、未解決の研究課題でも評価するようになっています。OpenAIは2026年5月にも、数学者ポール・エルデシュが提唱した単位距離予想を未公開モデルが反証したと報告していました。

OpenAIが80年近く未解決だった数学予想の反証に成功、人間の数学者も「AIが補助役を超えた」と驚く発見 - GIGAZINE

今回の発表は未公開モデルを複数分野の未解決課題に取り組ませ、得られた成果のうち10件をまとめて公開するものです。

OpenAIによると、Astraが生成した数学的な議論は人間の担当者によって論文原稿にまとめられ、その後Astraがそれぞれの議論について、定理や前提条件を厳密な記号で記述して推論の各段階が規則に従っているかをコンピューターで確認するソフトウェア「Lean 4」で形式化したとのこと。GitHubで公開されたリポジトリには10件分のLean形式の証明データに加えて、証明全体を構築する手順や独立検査用ツールの案内も収録されています。

GitHub - openai/ten-proofs: Lean certificates accompanying proofs in mathematics and theoretical computer science · GitHub
https://github.com/openai/ten-proofs

OpenAIが公開した10件の成果は以下の通り。

・高次元の球充填密度の上限を、コーン―エルキース法で得られる限界値まで改善
・二元符号と球面符号の最大規模について従来より指数関数的に強い上限を導出
・有限置換による近似ができない非ソフィック群を構成
・特定の群が対応する群フォン・ノイマン環によって一意に決まるとするコンヌの剛性予想への反例
・行列のパーマネントを計算する算術回路と算術式について新たな計算量の下限を証明
・量子もつれを利用する任意の有限な2人ゲームについて指数関数的な並列反復定理を証明
・最近ベクトル問題について格子の次元に対して多項式倍の誤差を許しても近似が難しいことを証明
・重心だけが内部格子点となる凸体についてエールハルトの体積予想を全ての次元で証明
・多色三角形ラムゼー数について超指数関数的な下限を証明
・極値グラフ理論におけるコンパクト性予想と退化度に関する予想に対しそれぞれ反例を構成

二元符号と球面符号では高次元における一般的な上限をそれぞれ1977年と1978年以来初めて改善したほか、球充填でも一般的な高次元指数を1978年以来初めて改善したとのこと。量子計算量理論では、同じゲームを並列に繰り返した際に全てのゲームに勝つ確率が指数関数的に低下する「並列反復定理」を、量子もつれを利用する任意の有限な2人ゲームまで拡張したと述べられています。

解法探索に必要だった総トークン数をOpenAIの「Sol API」の料金に当てはめると約2000ドル(約31万円)になるとのこと。

OpenAIは元の思考過程の記録や完成した論文などを別のAIモデルに読ませて証明へ至る流れを再構成した(PDFファイル)解説資料も公開しています。解説資料は元の思考過程の記録をそのまま掲載したものではなく、失敗した方針や視点の転換、最終的な着想を読みやすい解説として整理したものとなっています。

一方で「数学AIの普及後も人間が従来通り数学を続けられるとは限らない」と主張する論考も登場しています。論考では、数学は科学や工学に応用されるためチェスのように閉じた活動ではなく、AIが人間の理解を介さずに数学・科学・工学を進める可能性があると論じられています。

OpenAIは数学的な議論自体をAstraが生成したと明記し、論文原稿の作成とLeanによる形式化に関与したOpenAIが、証明の正しさに責任を負うと述べています。Astra自体の公開に先立って10件の証明が公開された形で、今後は数学界が各成果を既存研究の中に位置付け、新たな研究へつなげることを期待しているとのことです。