OpenAI「Astra」が数学の未解決問題10件で解決・大幅進展：全件にLean 4証明書、探索コストは約2,000ドル
2026年8月1日、OpenAIは「Ten advances in mathematics and theoretical computer science」を公開し、未公開の次期主力モデルAstraの内部版が数学・理論計算機科学の未解決問題10件を解決または大幅に前進させたと発表した。初版原稿は249ページで、10件すべてのLean 4形式証明がGitHubで公開されている。原稿はその後、8月6日の改訂で253ページになった。
これまでのAIによる数学の成果発表は「本当に正しいのか」を人間が読んで確かめるしかなかった。今回はそこが違う。Leanのカーネルは証明を受理するか拒否するかの二択しか返さない。検証は、人間が数百ページの証明を一から追う作業から、機械的な型検査へ移せる。少なくとも形式化された定理と証明については、AI自身の自己申告ではなく、Leanカーネルが受理したものとして確認できる。
そしてこのニュースの本当に面白い部分は、発表の2日後から起きた。
サマリー
| 論点 | 内容 |
|---|---|
| 何が起きたか | 未公開モデルAstraが未解決問題10件を解決または大幅に前進。Erdős問題146・180・183を含む |
| 検証方法 | 10件全件にLean 4証明書。合計548,205行、sorry（証明の穴）ゼロ |
| コスト | 解を見つけるまでのトークン代はGPT-5.6 Sol換算で約2,000ドル |
| 論争 | 先行研究の帰属をめぐり公式サイトの一文が8月3日に撤回、8月6日に原稿改訂 |
Astraとは何か
OpenAIは公式ページで「これらの結果は、次期主力モデルであるAstraの内部版によって達成された」と書いている。Astra自体は未公開で、公開時期のアナウンスもない。現時点で外部から触れる手段はない。
コスト表記に使われている「Sol API rates」は、現在のGPT-5.6 Solの標準API料金（入力$5 / 出力$30 per 1Mトークン）を基準にコスト換算したという意味だ。AstraとSolのモデル系譜上の関係について、OpenAIは明らかにしていない。公式が述べているのは、Astraが「our next major model（次の主要モデル）」であることまでで、GPT-5.7相当なのか、次世代のSolなのか、別系統なのかは現時点では確認できない。
解決された10件
OpenAI公式および原稿の要旨に基づく一覧が以下になる。
| # | 問題 | 結果 |
|---|---|---|
| 1 | 高次元球充填 | Cohn–Elkies線形計画の漸近的な強さを厳密に決定。指数は α* = 0.6044… |
| 2 | 二元符号・球面符号 | 任意の最小距離について、古典的上界を指数因子で改善 |
| 3 | 非ソフィック群 | 非ソフィック群を明示的に構成。二元Leavitt代数の単元群とThompson群 V を使用。問題自体はGromov（1999）・Weiss（2000）に帰される |
| 4 | Connesの剛性予想 | 同じ群フォンノイマン環を持つ、互いに非同型な性質(T)群を無限個構成し反証 |
| 5 | 算術回路計算量 | パーマネントについて除算なし回路は Ω(n² log log n) ゲート、式は Ω(n⁴/log n) 葉が必要 |
| 6 | 量子並列反復 | 任意の有限2プレイヤーもつれゲームに対する指数的並列反復定理 |
| 7 | 最近ベクトル問題 | 3SATからの直接還元により n^(1/400) 因子の近似困難性 |
| 8 | Ehrhartの体積予想 | 重心が唯一の内部格子点である凸体の体積上界 (n+1)ⁿ/n! を全次元で証明 |
| 9 | 多色Ramsey数 | R_k(3) = k^Θ(k) の超指数的下界（Erdős問題183） |
| 10 | コンパクト性・退化予想 | Erdős–Simonovitsのコンパクト性予想とErdősの退化予想を反証（Erdős問題146・180） |
ここで注意しておきたいのは、10件が同じ強さの主張ではないことだ。OpenAIの表現は「それぞれが長年の未解決問題を解決する、または大幅に前進させる」であり、個々の結果がどちらなのかを公式は一つずつ明示していない。原稿要旨の動詞を手がかりに本稿で整理すると、次のように読める。
| 性格 | 該当 | 根拠となる原稿の表現 |
|---|---|---|
| 問いに決着 | 3・4・8・9・10 | 「構成される」「反証する」「証明される」。Erdős問題146・180・183は公式が「resolving」と明記 |
| 当該の問いには決着、ただし上位の問題は未解決 | 1・6 | 線形計画の漸近レートを「厳密に決定」、並列反復定理を「証明」。球充填問題そのものが解けたわけではない |
| 既存の上界・下界の改善 | 2・5・7 | 「指数因子で改善される」「〜が必要」「〜の困難性を与える」 |
たとえば5のパーマネントの下界は超多項式ではなく、VP対VNPの分離には届かない。7も多項式因子の困難性であって、格子暗号の安全性議論を書き換えるものではない。「10件すべてが未解決問題の解決」と要約すると実態より強くなる。
分野は高次元幾何、符号理論、算術回路計算量、群論、作用素環、量子計算量、格子暗号、極値組合せ論にまたがる。単一分野への特化ではなく横断的だという点が、モデルの汎用性を示す材料としてOpenAI側の主張の軸になっている。
いくつか補足しておくと、球充填の結果についてOpenAIの原稿は「一般の球充填指数に対する1978年以来初の改善」と述べている。従来のKabatianskii–Levenshtein指数は 0.59905576… で、以降の改良は低次の因子に留まっていた。また最近ベクトル問題は格子暗号（ポスト量子暗号）の安全性の根拠に関わる問題で、10件のうち実務との距離が最も近い。
Lean 4証明書：548,205行、sorryゼロ
リポジトリ openai/ten-proofs はApache-2.0で公開され、Lean 4.32.0とmathlibでビルドできる。今回、公開されている10ファイルを実際に取得して行数とsorry（未証明箇所を許すLeanのプレースホルダ）の出現数を数えてみた。
| ファイル | 行数 | sorry |
|---|---|---|
| GapCVP.lean | 130,430 | 0 |
| MetricCodes.lean | 114,406 | 0 |
| QuantumParallelRepetition.lean | 70,980 | 0 |
| EhrhartVolumeInequality.lean | 55,755 | 0 |
| SpherePacking.lean | 55,616 | 0 |
| ConnesRigidity.lean | 37,374 | 0 |
| NonSoficGroup.lean | 34,440 | 0 |
| Permanent.lean | 27,563 | 0 |
| CompactnessAndDegeneracy.lean | 18,588 | 0 |
| MulticolorTriangleRamsey.lean | 3,053 | 0 |
| 合計 | 548,205 | 0 |
sorryが一つでも残っていれば「その部分は未証明」を意味するので、ゼロであることは少なくとも明示的な証明穴を残していないことを示す。ただし保証されるのはそこまでだ。形式化された定理が意図した数学の問題と同じものか、定義の置き方が標準的な理解と一致するか、依存する公理が適切か──これらはsorryの有無とは別の問題として残る。
その隙間を埋めるために用意されているのが ComparatorChallenges/ ディレクトリだ。Comparator はLean開発チームのリポジトリで公開されている検証ツールで、READMEは自らを「Lean証明のための信頼できる審判（a trustworthy judge for Lean proofs）」と説明している。指定した定理について保証するのは次の3点だ。
- Challengeファイルに書かれた定理文と同じ命題を証明していること
- 許可リストにある公理以外を使っていないこと
- Leanカーネルに受理されること
OpenAIが同梱した設定ファイルは12件（一部の結果が2ファイルに分かれている）ある。全件を取得して確認したところ、permitted_axioms はいずれも propext・Quot.sound・Classical.choice の3つだけだった。Lean/mathlibの標準公理であり、独自の公理を持ち込んでいないことになる。また全件で enable_nanoda が true に設定されていた。Lean本体とは別実装の nanoda カーネルでも検査する設定だ。対象定理は合計38件になる。
つまり「OpenAIの手元でLeanが通りました」ではなく、定理文・使用公理・カーネル受理の3点を第三者が独立に確認できるところまで用意されている。これは形式化の完全性そのものの証明ではないが、検証可能性への配慮としては現時点でかなり踏み込んだ部類に入る。
もっともComparatorも「何も信頼せずに検証できる」道具ではない。READMEは保証の前提を6点列挙しており、Challenge側のimportsとlakefileが検証者の管理下にあること、サンドボックスが正しく機能すること、そしてカーネルが正しいことなどが含まれる。興味深いのは最後の前提で、enable_nanoda を有効にすると「Leanカーネルとnanodaカーネルのどちらかが正しければよい」に弱められるとREADMEは書いている。OpenAIが12件すべてでこれを有効にしているのは、その分の担保まで取りにいった形になる。
約2,000ドルという数字の読み方
OpenAIは「これらの問題の解を見つけるのに必要だったトークン総数は、Sol API料金で約2,000ドルに相当する」と書いている。Solの標準単価は入力$5 / 出力$30 per 1Mトークンなので、これで割り戻すと次のようになる。
| 仮定（標準単価での単純換算） | トークン量 |
|---|---|
| 全額が出力トークンだった場合 | 約6,700万トークン |
| 全額が入力トークンだった場合 | 約4億トークン |
ただしこれは厳密な上下限ではない。OpenAIの料金表はSolを短コンテキストと長コンテキストの2段階で掲載しており、入力が一定長を超えると長コンテキスト料金（入力$10 / 出力$45）がリクエスト全体に適用される。キャッシュ入力やBatch APIを使えば逆に単価は下がる。数千万〜数億トークンという桁感の目安として読むのが妥当なところだ。
そのうえで、この数字が何を指しているかを整理しておきたい。「2,000ドル」はAstraの学習費や人間の作業費ではなく、OpenAIが「解を見つけるのに必要だった」とするトークン数をSol API料金で換算した値である。失敗試行や探索過程をどこまで含むかは公開されていない。原稿化と形式化に費やされた人間側の工数も、当然ここには入らない。
誰が何をやったのか
OpenAIはワークフローを次のように説明している。
- Astraが数学的な議論そのものを生成する
- 同じモデルを使って、人間が原稿を整える
- モデルが各議論をLean証明書に形式化する
そのうえで公式ページはこう書いている。「私たちは原稿の準備とLeanでの形式化を手伝い、その正しさに責任を持つ。一方で数学的な議論そのものは我々のシステムが生成した」。
帰属についての姿勢も明示された。「AIシステムが全面的に生成した証明について人間の著者性を主張することは、システムの貢献と人間の真の知的作業の性質の双方を誤って表現することになる」。だから人間を著者に立てない、という論法だ。今回の原稿に人間の著者名はなく、非ソフィック群の章では Henry Bradford、Michael Chapman、Alon Dogon、Francesco Fournier-Facio、Andrei Jaikin-Zapirain、Gábor Kun、Andreas Thom への謝辞が記されているが、彼らは著者ではなく「有益なコメントをくれた人」として扱われている。
発表の2日後に起きたこと
ここからが今回のニュースの核心になる。
8月3日、数学者 Francesco Fournier-Facio が arXiv に「A torsion-free non-sofic group」（arXiv:2608.02025）を投稿した。4ページの短報で、要旨はこう始まる。「OpenAIは非ソフィック群の存在を発表した：二元Leavitt代数の単元群である」。そのうえで同じ技術的判定条件を使い、捩れのない（torsion-free）非ソフィック群という別系統の例を構成してみせた。発表から中1日で、人間の数学者がその結果を土台に次の論文を書いたことになる。
同じ論文の脚注には、批判も書かれていた。証明の鍵となる技術的道具は Kun（2016）と Kun–Thom（2019）の仕事に決定的に依拠しているのに、OpenAIの8月1日の発表は「主要な結果について少なくとも10年間進展がなかった」と述べていた、という指摘だ。そして脚注は続ける──「この主張は8月3日に撤回された」。
実際、現在のOpenAI公式ページを取得して確認したところ、この一文は本文中に存在しない。
さらに8月6日、原稿そのものが改訂された。現行版は脚注に「Updated August 6, 2026」と明記し、原版へのリンク（ten-proofs-oai-original.pdf）を併記している。両方を取得して比較したのが下表になる。
| 版 | ページ数 | PDF作成日時 |
|---|---|---|
| 原版 | 249 | 2026-08-01 17:29 JST |
| 現行版 | 253 | 2026-08-06 07:47 JST |
4ページの増加は誤字修正の規模ではない。要旨を比較すると、非ソフィック群の項目が次のように書き換えられている。
| 版 | 非ソフィック群の記述 |
|---|---|
| 原版（8月1日） | 「議論は性質(T)エクスパンダーと二元Leavitt代数を用いる」 |
| 現行版（8月6日） | 「証明は KunおよびKun–Thomの仕事 と、組合せ的なエクスパンダー・マッチング論法を組み合わせ、二元Leavitt代数とThompson群 V を用いて実現される」 |
本文側でも Kun への言及が大幅に増え、Kun の定理と Kun–Thom の定理が「外部からの入力（external inputs）」として明示的に定理番号付きで整理し直されている。批判を受けて先行研究の位置づけを直した、という経緯が原稿の差分にそのまま残っている形だ。
ライデン宣言との緊張関係
OpenAIが公式ページで名指しで言及しているのが、2026年6月2日に公開された ライデン宣言（Leiden Declaration on AI and Mathematics） だ。オランダ・ライデンのLorentz Centerで2025年9月に開かれた会議を起点とし、国際数学連合（IMU）が支持を表明している。
宣言が挙げる懸念は5点ある。
- 現行の自動化手法は、もっともらしいが信頼できない議論を生成しうる
- AIモデルは統合元の人間の研究を適切に引用しないことが多い
- AIで解ける問題に研究の重心が寄り、動機が歪む
- プレスリリースによる発表が査読を迂回する
- 産業界の関与が研究の自律性を脅かす
今回の一件は、この2番目と4番目がそのまま現実化したケースだと言える。帰属の記述は実際に問題視されて撤回・改訂されたし、10件はいずれも査読を経ていない。
一方で1番目の懸念については、Lean証明書とComparator設定という形で正面から応答している。「もっともらしいが誤った議論」を機械的に弾く手立ては用意された、という段階だ。宣言の指摘のうち「正しさの担保」には具体的な回答が示され、「帰属」と「査読」は未解決のまま、という整理になる。
まだ言えないこと
過大評価を避けるために、明示しておくべき限界がある。
Lean検証と数学的受容は別物だ。 Leanが保証するのは「形式的に書かれた命題からその証明が導かれる」ことであって、「その形式的命題が、分野の人が関心を持っている問題と同じものか」は人間が判断するしかない。前述のComparatorもこの隙間は埋めない。Comparatorが保証するのはSolutionがChallengeと同じ命題を証明していることであって、そのChallengeの定理文が数学者の考えている問題を正しく写しているかは検証範囲の外にある。定義のエンコードが標準的な用法と一致しているか、非形式的な導入部と形式的な定理の接続に飛躍がないか──ここは依然として人間のレビュー領域になる。
加えて、モデル本体は非公開で、学習データも計算資源の詳細も外部からは見えない。再現実験は不可能で、検証できるのは出力された証明だけだ。10件のバンドル全体について独立した専門家レビューや査読付き出版は、本稿執筆時点で確認できていない。
そして今回の10件にミレニアム懸賞問題は含まれていない。いずれも「長年開いていた良質な問題」であって、分野そのものを定義するレベルの大問題ではない。
なぜこれが今後の基準になるのか
今回の発表には前例がある。OpenAIは2026年5月、Erdősの単位距離予想の反証を未公開モデルで得たと公開していた。公式ページの脚注によれば、この結果はすでに5本の後続論文を生んでいる（Bloom–Sawin–Schildkraut–Zhelezov、Pohoata、Saha–Xu–Ye、Goh–Hatami、Lee–Pohoata–Zhu）。
つまりパターンが繰り返されている。AIが結果を出す → 人間が数日〜数週間で拡張論文を書く → その拡張がまた次を生む。Fournier-Facioの2日後の投稿は、このサイクルがさらに短くなっていることを示している。
エンジニアの視点で押さえておきたいのは、「検証可能な形式で成果を出す」ことが、AI生成物の信頼性問題に対する現時点で最も強い回答になっているという点だ。数学におけるLean証明書は、コードにおけるテストスイートや型システムに相当する。モデルが賢くなるほど出力の検証コストが問題になるが、機械可読な正しさの証明を同時に吐かせれば、検証は人間のレビューから機械的なチェックに移せる。この構図は数学に限った話ではない。
なおOpenAIは同じページで、10万人の科学者・数学者に最良のChatGPTモデルへの無料アクセスを提供する「ChatGPT for Academic Researchers」にも触れている。研究コミュニティとの緊張を抱えながら、同時にコミュニティへの浸透を進める動きが並行している。
まとめ
- OpenAIは2026年8月1日、未公開の次期主力モデルAstraが数学・理論計算機科学の未解決問題10件を「解決または大幅に前進させた」と発表。Erdős問題146・180・183を含み、分野は高次元幾何から格子暗号まで8領域にまたがる
- 10件全件にLean 4証明書が付き、合計548,205行に
sorryが一つもない。これは明示的な証明穴がないことまでを示す - 検証ツールComparator用の設定も12件同梱され、定理文の一致・使用公理・カーネル受理を第三者が独立に確認できる。許可公理は全件でLean標準の3つのみ
- 「解を見つけるのに必要だった」トークン数をSol API料金で換算すると約2,000ドル。学習費や人間の作業費は含まず、失敗試行や探索過程をどこまで含むかは公開されていない
- 帰属をめぐり「10年間進展がなかった」という記述が8月3日に撤回され、8月6日には原稿がKun・Kun–Thomへの帰属を大幅に補強する形で改訂された
- 発表2日後にFournier-Facioが拡張論文をarXivに投稿。ライデン宣言が示した懸念のうち「正しさ」はLeanで応答された一方、「帰属」と「査読」は未解決のまま残っている
情報ソース：