OpenAIの未公開AI「Astra」が未解決問題10問を解いた──機械検証付きの証明を読む

2026年8月1日、OpenAIは「数学と理論計算機科学における10の進展」と題した249ページの論文集を公開した。著者は同社の次期主力モデルとされる「Astra」の内部版で、扱われているのは球の詰め込み・非ソフィック群の存在・多色ラムゼー数など10個の未解決問題。いずれもOpenAI自身の説明では「主結果について少なくとも10年間、進展が見られなかった」問題だという。この記事は2026年8月2日公開の動画「OpenAIの未公開AI『Astra』、数学の未解決問題を10問解決」の内容を、公開後にあらためて一次資料を確認しながら整理したもの。なお、OpenAI自身の発表ページ(openai.com)は本記事の執筆時点で直接アクセスできず(403エラー)、GitHubで公開されている証明書リポジトリと、OpenAIの原文を引用している技術ブロガーSimon Willison氏の記事で裏付けを取っている。

• 10問すべてに、証明を一行ずつ機械的に検査するLean 4形式の検証済み証明書が付き、GitHubのopenai/ten-proofsリポジトリで公開されている
• 1955年から70年以上未解決だった多色ラムゼー数の下界を更新し、Erdős(エルデシュ)が1955年当時に250ドルの懸賞を懸けていた問題を解決した
• OpenAIによれば1問あたりのコストはGPT-5.6 Solのトークン価格換算で2,000ドル未満。ただし他に何問挑戦して解けなかったかは公表されていない

発表の概要

何が公開されたのか

OpenAIの発表原文には、本記事の執筆時点でアクセスできなかった(403エラー)。ただしGitHubのopenai/ten-proofsリポジトリは「Lean certificates accompanying ten proofs in mathematics and theoretical computer science(数学と理論計算機科学における10の証明に付随するLean証明書)」と説明されており、実際に10問分の形式的証明が公開されている。論文本体のPDF(cdn.openai.com/pdf/ten-proofs-oai.pdf)は直接取得でき、冒頭のAbstractには10問の一覧が並ぶ。1問目は高次元での球充填問題、3問目は「あらゆる可算群はソフィックか」という長年の問いに答える非ソフィック群の構成、9問目はk色ラムゼー数R_k(3)が超指数関数的に増加することを示す下界の証明、10問目はErdősとSimonovitsのコンパクト性予想への反例構成、といった具合に分野は多岐にわたる。このPDFの1ページ目には「2026年8月6日に更新。初版はten-proofs-oai-original.pdfで参照可能」という注記があり、公開後に一度改訂されていることが分かる。

技術ブロガーのSimon Willison氏は、OpenAIの発表原文を直接引用する形で「次期主力モデルAstraの内部版に、主結果について少なくとも10年間進展が見られなかった10の数学的問題を解かせた」「1問あたりGPT-5.6 Solのトークン価格換算で2,000ドル未満を費やしたと主張している」と紹介している。同氏はこれに続けて「(何問に2,000ドルを費やして解けなかったかについては情報がない)」と皮肉交じりに指摘しており、成功した10問の裏でどれだけの失敗があったかは公表されていない。

70年物の懸賞問題と、存在するかどうかも不明だった対象

論文集の第9章が扱う多色ラムゼー数の問題は、3色以上で点をつないだグラフを塗り分けたとき、必ず同じ色の三角形ができてしまう境目の数(R_k(3))がどう増えるかを問うものだ。論文本文には「Erdősは(1)の値を決定した者に250ドルを、有限かどうかを判定した者に100ドルを提供した」と明記されている。この懸賞は1955年のGreenwood–Gleasonの論文に遡り、70年以上にわたって上界(階乗のオーダー)と下界(指数関数のオーダー)の間にギャップが残っていた。OpenAIの論文は、このギャップのうち下界側を「k^Θ(k)」という超指数関数的な形にまで押し上げたと主張している。

もう一つ、論文集の第3章が扱う非ソフィック群は、「果たしてそのようなものが存在するのか」という問い自体が長年未解決だった対象だ。論文はKunとKun–Thomの先行研究を組み合わせ、binary Leavitt代数とThompson群Vを使った具体的な構成によって、非ソフィック群が実在することを示したとしている。

機械検証は何を保証するのか

AIが「証明した」と主張しても、それが本当に正しいとは限らない。今回の10問すべてに、証明の一行一行を機械的にチェックするLean 4という形式検証システムを通した「証明書」が付いている点が、この発表の核になっている。GitHubリポジトリには実際にLeanのコードが公開されており、これは著者(OpenAIないしAstra)の自己申告ではなく、独立したソフトウェアによる論理チェックを経ているという意味になる。数学の世界でコンピュータ支援証明が大きな論争を呼んだ前例としては、1976年のAppel–Hakenによる四色定理の証明があり、今回はその流れの延長線上にある。

なお、Sebastien Bubeck氏(OpenAIの研究者)がこの発表についてX(旧Twitter)で投稿し、大きな反響を呼んだと伝えられているが、その投稿の閲覧数についてはX側の仕様上、本記事の執筆時点で筆者が直接確認する手段がなかった。反響があったこと自体は複数の技術系ニュース・ブログで言及されているが、具体的な数値は未確認として扱う。

この能力が実務にどうつながるかもしれないのか

数学の未解決問題を解く能力そのものより重要だとされるのは、AIが数日間にわたって自力で計画を立て、試行錯誤し、失敗を修正しながら最後までやり切ったという点だ。数学の証明は、長い知的作業を一つも間違えずに積み上げる能力を測る難関のテストケースとして扱われている。もしこの能力が他の領域にも及ぶなら、現在の「メールを書く」「調べる」といったタスク単位の指示から、「確定申告を丸ごと片付ける」「調査を解決まで進める」といったプロジェクト単位の依頼へと、AIの使い方が変わる可能性がある――という見立てが動画の主旨である。

過去の実績として、OpenAIのo3は2024年12月の発表から2025年4月の一般公開まで約4か月だった。ただし、これは1つの前例にすぎず、Astraが同様のペースで一般公開されるかどうかは現時点で分からない。実際、この動画の公開から6日後の2026年8月7日、OpenAIはAstraのサイバー能力が自社の安全基準の最上位「Critical」に達した可能性を排除できないとして、Astra関連の一部社内作業を一時停止したと発表している。詳細はOpenAI、次世代モデル「Astra」の開発を一時停止にまとめてある。数学の証明能力とサイバー能力は別の評価軸だが、同じAstraという内部モデルについて、公開からわずか1週間足らずで安全面の懸念が公式に表明されたことは、本記事の内容とあわせて押さえておく価値がある。

「かもしれない」の範囲であることを断った上での応用先

以下は動画が紹介する応用の可能性であり、いずれも実現するかどうか、実現時期がいつかは未確定の話として扱う。

AIが全論文・全データを横断的に読み込む能力が育てば、原因の仮説が割れたままの病気の解明が進むかもしれない、という期待がある。厚生労働省が2024年に公表した推計では、2025年時点で認知症の高齢者は約471.6万人、軽度認知障害(MCI)を合わせると約1,035.9万人にのぼるとされている。この分野での前例としては、タンパク質の立体構造という50年来の課題を解いたAlphaFoldが2024年のノーベル化学賞を受賞している。同様に、素材探索の分野ではGoogleのGNoMEが約38万1千件の新しい安定素材候補をNature誌上で報告しており(2023年)、人間だけでは試しきれない組み合わせ空間をAIが探索した先例として位置づけられる。

物理学の分野では、宇宙の大部分を占めるダークマター・ダークエネルギーの正体、あるいは1859年から未解決のリーマン予想といった大きな問題も引き合いに出されているが、これらはあくまで「もし今回のような能力が育てばどうなるか」という願望的な将来像であり、Astraがこれらの問題に取り組んだという事実はない。

確認できなかったこと・限界

OpenAIの公式発表ページ(openai.com)は、本記事の執筆時点で403エラーによりアクセスできなかった。本文中でOpenAIの発表内容として紹介した引用は、GitHubリポジトリの記述、および原文を直接引用しているSimon Willison氏のブログ記事を通じて確認したものであり、OpenAIの公式ページそのものを筆者が直接閲覧したわけではない。Sebastien Bubeck氏のX投稿の閲覧数については、X側の技術的制約により本記事執筆時点で確認できておらず、具体的な数値は本文に記載していない。「Astra」というモデル名が正式名称として維持されるか、いつ一般公開されるかもOpenAIから発表されておらず未確定である。OpenAIは他にどの未解決問題に挑戦して失敗したかを公表しておらず、成功率や試行回数は不明である。第6章・第7章で紹介した認知症解明・素材探索・物理学・暗号への応用は、いずれも動画が提示する将来の可能性であり、Astraの今回の成果がこれらに直接つながると確認されたものではない。

GitHubリポジトリと論文PDF、Nature・厚労省資料も参照

• openai/ten-proofs: Lean certificates accompanying ten proofs in mathematics and theoretical computer science | GitHub（2026年8月確認）: https://github.com/openai/ten-proofs
• Ten Advances in Mathematics and Theoretical Computer Science（PDF、2026年8月6日改訂版、2026年8月確認）: https://cdn.openai.com/pdf/ten-proofs-oai.pdf
• Ten Advances in Mathematics and Theoretical Computer Science | Simon Willison's Weblog（2026年8月1日、2026年8月確認）: https://simonwillison.net/2026/Aug/1/ten-advances-in-mathematics/
• Scaling deep learning for materials discovery | Nature 624, 80–85 (2023): https://www.nature.com/articles/s41586-023-06735-9
• 認知症及び軽度認知障害の高齢者数と有病率の将来推計（九州大学・厚生労働省補助事業、2024年公表、2026年8月確認）: https://www.mhlw.go.jp/content/001279920.pdf
• ノーベル化学賞2024（AlphaFold・Hassabis氏ほか）: https://www.nobelprize.org/prizes/chemistry/2024/press-release/