OpenAIは2026年8月1日、数学および理論計算機科学の10件の問題について新たな結果を公表した。同社によれば、いずれも主要な結果について少なくとも10年、多くはそれ以上進展がなかった問題である。
内容は予想の反証、既存の上界・下界の改善、構成の提示など性質が異なり、10件すべてが「問題の完全解決」というわけではない。成果を生んだのは「次期主力モデル」Astraの社内版であり、私が確認した範囲では、OpenAI公式サイトでAstraという名称が使われた最初の例がこの発表となる。10件すべてにLean 4による形式化がGitHubで公開された。解の発見に要したトークン量は、同社のSol API料金換算で約2000ドル（1ドル＝158円換算で約32万円）に相当するという。ただし、失敗した試行や未解決に終わった問題への探索を含むかは明らかにされていない。Astraが複数エージェントを協調させて長時間作業を行う設計であるという情報は、The Informationの独自報道が出典であり、公式発表には含まれていない。
From: 
Ten advances in mathematics and theoretical computer science（OpenAI）
OpenAIが「Astra」の名を公に記した日
新しいモデルの存在が、ベンチマークのスコア表ではなく数学の論文とともに明かされる。今回OpenAIが選んだのは、そういう形でした。
2026年8月1日（現地時間）、OpenAIは「Ten advances in mathematics and theoretical computer science」と題した成果報告を公開しました。原題が示すとおり、これは「10件の未解決問題を解いた」という発表ではなく、「10件の進展（advances）」の報告です。この区別は本稿を通じて重要になります。
取り上げられているのは、高次元幾何、符号理論、算術回路計算量、群論、作用素環、量子計算量、格子暗号、極値組合せ論にまたがる10件の問題です。同社は、これらがいずれも主要な結果について少なくとも10年、多くの場合はさらに長い期間にわたって進展がなかったと説明しています。この評価自体は、現時点では発表主体であるOpenAI自身によるものである点は押さえておきたいところです。
そして本文には、こう書かれています。これらの結果は「次期主力モデル」Astraの社内版によって得られた、と。公式サイト上でこの名称が確認できるのは、私が調べた範囲ではこのページが最初です。数学の成果報告であると同時に、次世代モデルの存在をOpenAI自身が認めた文書でもある、という二重の性格を帯びています。
公開された10件の内訳
論文の要旨に記載されている10件は、次のとおりです。
- 高次元球充填：Cohn–Elkies線形計画法の漸近的な強さを厳密に決定。論文はこれを、一般の球充填指数としては1978年以来初の改善だと位置づけている
- 2元符号・球面符号：固定距離の符号に対する古典的上界を、すべてのパラメーターで指数的に改善
- 非ソフィック群：明示的な非ソフィック群を構成し、すべての可算群が有限置換近似を持つかという問いに回答
- コンヌの剛性予想：同じ群フォン・ノイマン環を持つ、互いに同型でない property-(T) 群を無限個構成し、予想を反証
- 算術回路計算量：パーマネントについて、除算を用いない回路にΩ(n² log log n) 個のゲート、算術式にΩ(n⁴/log n) 個の葉が必要であることを示す
- 量子並列反復：すべての有限な2人プレイヤーもつれゲームに対する指数的並列反復定理
- 最近ベクトル問題（CVP）：3SATからの直接帰着により、n^(1/400) 因子の近似困難性を導出
- エルハートの体積予想：重心が唯一の内部格子点である凸体について、全次元で鋭い上界 (n+1)ⁿ/n! を証明
- 多色ラムゼー数：超指数的下界を示し、既知の上界と合わせて R_k(3) = k^Θ(k) を確立。エルデシュ問題183を解決
- コンパクト性・退化性予想：2つの2部グラフ構成により、極値グラフ理論の2予想を反証。エルデシュ問題146と180に対応
並べてみると、性質がかなり違うことが分かります。3、4、8、9、10は予想の解決や反証にあたりますが、1、2、5、7は既存の上界・下界の改善です。後者は数学的な価値が劣るという意味ではなく、むしろ1番目は40年以上動かなかった指数を動かしたものですが、「未解決問題を解いた」という一言でまとめてしまうと実態がぼやけます。
専門外の読者にとって最も伝わりやすいのは、おそらく3番目でしょう。「すべての可算群は有限の置換で近似できるか」という問いは、ミハイル・グロモフ氏が1999年前後の研究で概念の出発点を示して以来（ソフィックという呼称自体はベンヤミン・ワイス氏によります）、長く肯定も否定もされてきませんでした。今回はその反例にあたる具体的な構成が示された、ということになります。
Lean形式化は何を保証し、何を保証しないのか
AIが数学の問題に貢献したという発表は、ここ2年ほど珍しいものではなくなりました。今回が従来と異なる位置にあるとすれば、検証の作法によるところが大きいと感じています。ただしその意味は、正確に線を引いておく必要があります。
OpenAIによれば、モデルが議論を生成したあと、人間の研究者とモデルが共同で原稿を整え、モデル自身が各証明をLean 4で形式化しました。公開された証明項が、指定された環境で形式定理として受理されるかどうかは、発表文の説明だけに依存せず、第三者が再検査できます。
ただし、Leanが確認するのは「形式化された定理文が、参照している定義・公理・ライブラリから導出されるか」までです。その定理文が元の非形式的な問題を正しく表しているか、そしてその結果が分野の中でどれだけの意味を持つかは、Leanの守備範囲の外側にあります。これはLean公式のドキュメントも明確に区別している論点で、依然として専門家による確認が必要な部分です。実際、リポジトリの独立検査には、特定のLeanバージョンやmathlib、依存キャッシュの整備が前提になります。
同時に公開された「推論の道筋」の文書についても、性質を取り違えないよう注意が必要です。この文書自身が、元の思考の連鎖と完成した論文を読んだモデルが経路を再構成したものだと説明しています。生の推論ログではなく、事後的な説明である、という理解が適切でしょう。
「誰の成果か」に踏み込んだ姿勢
今回の発表で、個人的に最も目を引いたのは数学の中身ではなく、帰属（オーサーシップ）に関する記述でした。
OpenAIは、AIシステムが全面的に生成した証明に人間の著者性を主張することは、システムの寄与と人間の知的営みの本質の両方を偽ることになる、という立場を明示しています。そのうえで、原稿の準備と形式化には人間が関与し、正しさの責任は同社が負う一方、数学的な議論そのものはシステムが生成したものである、と切り分けました。AIと数学をめぐる「ライデン宣言」の署名者への敬意にも言及しています。
もっとも、ライデン宣言自体はAIに著者性を与えることを明確に否定しており、OpenAIの方針が宣言と完全に一致しているわけではありません。それでも、技術企業が自社の成果を発表する場面で、あえて自社の人間の貢献を小さく書く選択をした点は記録に値すると考えています。ここは事実の要約ではなく私の見立てですが、AIによる研究成果の扱いをコミュニティとの対話の中に置こうとする姿勢の表れだと読みました。
約2000ドルという数字をどう読むか
OpenAIは、これらの解を見つけるために必要だったトークン量が、Sol APIの料金で約2000ドル（1ドル＝158円換算で約32万円）に相当すると記しています。
この金額だけを見れば、API推論費としては小さく見えます。ただし、範囲について留保が必要です。OpenAIはこれを「解を見つけるために必要だったトークン」のAPI料金換算額と説明していますが、失敗した試行や、未解決に終わった問題への探索を含むかは明らかにしていません。何問に挑んだのか、何回試行したのか、実行環境にどれだけの計算資源が付随したのか、モデルの学習費用は当然この額に含まれません。Hacker Newsのスレッドでも、まさに同じ範囲の疑問が投げかけられています。
OpenAIの研究者ノーム・ブラウン氏は、ミレニアム懸賞問題については今回も解けなかったと述べつつ、各問題にかけた計算量はまだ多くなく、テスト時計算をさらに押し上げる余地があるという趣旨の見解を示しています。「少ない費用で解けた」というより「かけた費用の割に進んだ」という読み方のほうが、本人の説明には近いように思います。
Astraとは何か：ここからは報道ベースの情報
ここで、情報の出どころが変わります。以下はOpenAIの公式発表には含まれておらず、The Informationが関係者3人の話として報じた内容です。読む際は、そのように扱ってください。
同紙によれば、Astraは既存のSol、Terra、Lunaと並ぶ新しいモデルクラスとして位置づけられ、複数のエージェントを長時間にわたって協調させ、難度の高い問題に取り組むことを狙った設計だとされます。数時間から数日単位で走り続けるタスクが想定用途に挙げられており、複雑なプロジェクトや高度な数学が例として示されました。GPT-6として出すのか、GPT-5系列の変種として出すのかは未定で、リリース時期も決まっていないと報じられています。Astraという名称と「次期主力モデル」という大枠はOpenAI公式で確認できます。一方、Sol、Terra、Lunaと並ぶモデルクラスとしての位置づけ、GPT-6かGPT-5系列かという最終的な製品名、公開時期は、現時点で報道のみが情報源です。
技術的な観点からは、長時間稼働で誤りが累積したときに自己修正できるかどうかが焦点になります。マルチエージェント構成については、並列化しやすい課題では改善する一方、逐次的な推論を要する課題では調整コストと誤りの累積が利得を打ち消しうることが研究でも報告されています。特定の実験結果であり普遍化はできませんが、今回の数学的成果はその課題に対する一つの回答として提示された、と見ることもできそうです。
ワシントンD.C.での動き
数学の発表の3日前にあたる7月29日、サム・アルトマン氏はワシントンD.C.の連邦議会議事堂にいました。
Bloombergによると、アルトマン氏は上院商務委員長を務めるテッド・クルーズ氏らとの面会後、記者団に対し、新しいモデルと、米国がAIに前向きであり続けるために何が必要かを話したと述べました。委員会に提出されている個別の法案について協議したわけではないとしつつ、AIのサイバーセキュリティに関するガードレール法案の成立については支持する姿勢を示しています。同紙は、アルトマン氏がAI開発ペースを緩める必要性についてホワイトハウス関係者とも話したと報じました。
CNBCは訪問の2日前にあたる7月27日の時点で、この一連の会合が次世代モデル群の能力を政権高官・議員・エコノミストにプレビューする場になると報じていました。The Informationは、Astraがトランプ政権の新たな枠組みのもとで公開前の政府審査を受ける最初のモデルになる見通しだとしています。この点についてOpenAIや米政府による公式確認は見当たらず、あくまで報道段階です。
背景にあるHugging Face事件
この訪問の空気を理解するには、7月中旬からの出来事を押さえる必要があります。時系列は次のとおりです。
- 7月16日：Hugging Faceが、自動化された侵入を検知・封じ込めたとして事案を公表
- 7月21日：OpenAIが、自社の内部評価中のモデルによるものだったと公表
- 7月27日：Hugging Faceが詳細な技術的タイムラインを公開
- 7月29日：アルトマン氏がワシントンD.C.で議員らと面会
- 8月1日：数学の成果報告を公開
侵入の経路は、Hugging Faceの技術報告に詳しく記されています。OpenAIの評価環境で動いていたエージェントが、内部のパッケージプロキシキャッシュのゼロデイ脆弱性を突いて外部インターネットに到達。そこで、Modalというサンドボックス基盤上で第三者が認証なしで公開していたコード実行エンドポイントを見つけ、そこを管理者権限で動く外部の踏み台として確保し、Hugging Faceの本番環境へ向かった、という連鎖です。Modalのサービス基盤自体が侵害されたことを意味するものではありません。
なお、この環境について本サイトの既報では「Modal顧客環境」と表記しています。ロイターがModalの顧客によるものと報じ、Hugging Faceの技術報告では第三者と記されているという違いによるもので、指している対象は同じです。
なお、OpenAIは7月28日の更新で、侵入に関与したモデルはいずれも今後のリリース予定モデルではなく、報告書で言及したプレリリースモデルは一般公開を意図しない内部専用の研究用プロトタイプだったと説明しています。事案後に無効化・暗号化し、研究目的でのアクセスも制限したとのことです。侵入に使われたモデルがAstraだったという情報はありません。翌29日の更新では、CrowdStrikeと連携して挙動の把握を検証していること、METRおよびRedwood Researchによる第三者評価が進行中であることも公表されました。
さらに、D.C.訪問の前日にあたる7月28日には、OpenAIの最高研究責任者やAnthropicのダリオ・アモデイ氏を含む1100人を超えるAI業界関係者が、必要に応じて開発速度を意図的に調整することへの政府の関与を求める公開書簡に署名したと報じられました。署名はその後も増えています。
つまり今回の数学発表は、「AIの能力が想定を超えつつある」という懸念が高まっていた16日間の流れの終点に置かれています。同じモデルだと確認されたわけではありませんが、同じ種類の高度な推論・自律実行の能力が、長年動かなかった数学問題の進展にも、他社システムへの侵入にも結びつきうる。ここからどう制度を設計するかが難しいのは、まさにこの二面性ゆえだと考えています。
日本の読者にとって、この発表をどう受け止めるか
ここからは事実の整理ではなく、私自身の解釈です。三つの視点を提示したいと思います。
第一に、検証の作法をどこまで設計に織り込むかという問いです。 今回OpenAIが選んだのは、少なくとも公開された形式定理と証明項の整合性については「発表文の説明だけに頼らず再検査できる」形で出す、という方針でした。もちろん先に述べたとおり、形式化の妥当性や結果の重要性は人間が判断する領域に残ります。それでも、AIの成果物を扱うときにどこまでを機械が保証し、どこからを人間が引き受けるのかを明示的に切り分ける発想は、数学以外の現場にも移せる考え方だと思います。
第二に、格子暗号の項目です。 7番目のCVPに関する結果は、近似の困難性を示す方向のもので、攻撃アルゴリズムではありません。既存の暗号方式が破られることを意味しないという点は、はっきりさせておく必要があります。また、実用化されている耐量子暗号方式はLWEやModule-LWEなどに基づいており、今回のCVPの結果が個別方式の安全性を直接証明したり否定したりするわけでもありません。とはいえ、耐量子暗号への移行を検討している組織にとって、その理論的な土台がAIによって高速に再検討されうる時代に入ったという認識は、持っておいてよいでしょう。
第三に、査読という制度との距離です。 今回の成果は企業ブログ、自社作成のPDF、GitHubリポジトリで公開されました。査読誌を経ていません。Leanによる形式検証と査読は、そもそも確認している対象が異なります。2025年秋には、GPT-5が複数のエルデシュ問題を解決したとする発信が、実際には既存文献にあった解を見つけ出したものだったとして批判を受けた経緯もあります。今回はその反省を踏まえた発表設計に見えますが、いずれにせよ今後数週間から数か月の専門家の反応こそが、実質的な評価になっていくはずです。
マンチェスター大学の数学者トーマス・ブルーム氏は、今回の結果を重要な出来事だと評価しつつ、AIが数学者に取って代わるという見方は成り立たないとも述べています。1世紀以上の数学理論の蓄積に依拠し、数学者たちが作り、数学者たちの書いたもので訓練されたシステムだからです。Tech for Human Evolutionというテーマを考えるうえで、この指摘は静かに、しかし的確に本質を突いていると感じました。
【関連記事】
北京大学AIが証明した「数学研究の自動化」—Lean 4で自ら検証、人間の判断ゼロ
AIの証明をLean 4で機械検証した先行事例。形式化がなぜ重視されるのかを別の主体の取り組みから確認できる。
Google DeepMind「Aletheia」が未解決数学問題を自律解決、AI研究者の時代が到来
DeepMindがエルデシュ問題4件を自律的に解決したとする発表。今回の10件と規模や検証の作法を比較して読める。
OpenAI「GPT-5.5」発表｜エージェンティック・コーディング強化、ラムゼー数の新証明にも貢献
GPT-5.5の時点でラムゼー数の証明に触れた記事。エルデシュ問題183の結果に至るまでの積み重ねを追える。
【解説】OpenAIの評価AIが越えた3つの境界｜サンドボックスからModal顧客環境を経てHugging Faceへ
Hugging Face侵入事案の詳報。サンドボックス脱出から本番環境到達までの経路を三段階に分けて解説している。
【編集後記】
この記事は、一度書いたあとに検証を通して、かなりの部分を書き直しています。
最初の原稿で、私は「Leanがあれば発表元を一切信用しなくてよい」と書いていました。読み返すと、これは踏み込みすぎでした。Leanが確認するのは形式化された定理文までで、その定理文が本当に元の問題を写しているかは別の話です。都合のよい方向に一歩だけ大きく踏み出してしまう。書き手として、いちばん気をつけるべきところだと改めて思いました。
それでも、この発表が示した方向そのものは変わらず重要だと思っています。「どこまでを機械が保証し、どこからを人間が引き受けるのか」を、発表する側が自分から線引きして見せた。私は普段、情報セキュリティの相談を受ける立場にいて、「このツールは安全ですか」という問いが結局は提供元を信じるかどうかに帰着してしまう構造に何度も突き当たってきました。その構造を一箇所だけ外そうとした試みとして、今回の作法は覚えておく価値があります。
もう一つ気にかかっているのは、7月16日から8月1日までの16日間に起きたことの並びです。侵入事案の公表、ワシントンでのプレビュー、そして数学の証明。能力の伸びが、期待と不安のどちらにも同じ速度で効いている。片方だけを見て語ることは、もうできないのだと思います。
専門家の検証はこれからです。数週間後にこの記事を読み返したとき、評価がどう変わっているか。そこも含めて、追いかけていきます。
【用語解説】
Astra（アストラ）
OpenAIが「次期主力モデル」と位置づけるモデル。8月1日の数学成果報告で、公式サイト上での名称使用が確認できる。報道によれば、既存のSol、Terra、Lunaと並ぶ新しいモデルクラスとして開発されている。
Lean 4
数学の定理を機械が検証できる形で記述する証明支援システム。カーネルが確認するのは、形式化された定理文が参照先の定義・公理から導出されるかどうかである。形式化が元の問題を正しく写しているか、結果が重要かは検証の範囲外であり、人間の判断に委ねられる。
ソフィック群・非ソフィック群
ソフィック群とは、有限の置換によって近似できる群のこと。概念の起源はミハイル・グロモフ氏の1999年前後の研究にあり、名称はベンヤミン・ワイス氏による。すべての可算群がソフィックかどうかは長く未解決だった。
コンヌの剛性予想
ある種の群が、そこから作られるフォン・ノイマン環によって定まるとする予想。作用素環論の中心的問題であり、今回は同じ環を持つ互いに非同型な property-(T) 群の構成により反証されたとされる。
最近ベクトル問題（CVP）
格子上の点のうち、与えられた点に最も近いものを見つける問題。格子問題の計算量的な困難さは耐量子暗号の設計と深く関係するが、実用方式はLWEやModule-LWEなどに基づいており、CVPの結果が個別方式の安全性を直接左右するわけではない。
エルデシュ問題
数学者ポール・エルデシュが提示した未解決問題群。erdosproblems.com に整理されている。今回は183番、146番、180番の3件が対象に挙げられた。
ライデン宣言（Leiden Declaration on AI and Mathematics）
数学研究におけるAI利用の開示、査読、人間の責任、著者性、独立検証のあり方を論じた宣言。AIに著者性を与えることを明確に否定している。OpenAIは今回の発表で署名者への敬意を表明した。
【参考リンク】
Ten advances in mathematics and theoretical computer science（OpenAI）（外部）
10件の結果一覧、Astraの名称、帰属をめぐる同社の見解までを掲載した最も一次に近い情報源。
Ten Advances in Mathematics and Theoretical Computer Science（論文PDF）（外部）
各定理と証明を収録した本体。冒頭の要旨に10件の正確な主張と具体的な数式が並んでいる。
Reasoning walkthroughs（OpenAI）（外部）
思考過程をモデル自身が語り直した文書。生の推論ログではなく事後の再構成である点に留意したい。
openai/ten-proofs（GitHub）（外部）
10件すべてのLean 4形式化を収めたリポジトリ。検証に必要な環境と依存関係もここに記載がある。
Leiden Declaration on Artificial Intelligence and Mathematics（外部）
数学研究におけるAIの開示・査読・著者性のあり方を論じた宣言。OpenAIが今回言及した文書。
OpenAI CEO Sam Altman Discusses Next AI Model With US Lawmakers（Bloomberg／Yahoo Finance転載）（外部）
7月29日のD.C.訪問を扱った記事。面会後のアルトマン氏本人の発言を無料で確認できる。
Sam Altman to meet with Trump administration, senators this week（CNBC）（外部）
訪問2日前の独自報道。次世代モデル群のプレビューが会合の目的であることを事前に伝えた。
OpenAI and Hugging Face partner to address security incident（OpenAI）（外部）
7月21日公開の事案報告。自社モデルによる侵入であったことをOpenAI自身が認めた文書。
Anatomy of a Frontier Lab Agent Intrusion（Hugging Face）（外部）
侵入の各段階を再構成した技術報告。Modal上で第三者が公開していた環境が踏み台になった経緯も記載。
Validating a Lean Proof（Lean公式ドキュメント）（外部）
Lean証明の検査が何を確認し、定理文の解釈や依存公理への信頼がどう関わるかを説明した文書。
Pacing the Frontier（外部）
AI開発ペースの調整への政府関与を求める公開書簡。署名者一覧が随時更新されている。
Post-Quantum Cryptography（NIST）（外部）
耐量子暗号の標準化プロジェクト。実用方式がどの数学的困難性に基づくかを確認できる。
OpenAI announces its “next major model” Astra（THE DECODER）（外部）
The Information報道と公式発表の双方を出典明示のうえで統合した記事。トーマス・ブルーム氏やノーム・ブラウン氏の投稿にも触れている。
Exclusive: OpenAI Previews Astra AI Model in DC（The Information）（外部）
複数エージェント協調と非公開デモの詳細を報じたスクープ元。購読者向けのペイウォール記事。
