何が起きたのか

OpenAIが2026年8月1日、公式ページ「Ten advances in mathematics and theoretical computer science」で、内部モデル Astra が数学と理論計算機科学の10件の結果を出したと発表しました（OpenAI 2026-08-01）。いずれも主要部分に10年以上進展がなかった問題だとされています。

これまでのAI数学発表と決定的に違うのは、10件すべてに Lean 4 の機械検証可能な証明書が付いていることです。公式リポジトリ openai/ten-proofs には Lean 4.32.0 + mathlib による形式化が置かれ、lake exe cache get と lake build All で誰でも手元でビルドできます（openai/ten-proofs README）。論文本体は249ページで、10件すべての解の生成に要したトークンは Sol API レートで約2,000ドル相当だと報じられています（implicator.ai）。

この記事では「AIが数学を解いた」という見出しを、リポジトリの中身を実際に読むことで分解します。結論を先に言うと、このリリースで検証できる部分は過去のどのAI数学発表よりも厳密に検証でき、検証できない部分は依然としてはっきり残っています。そしてその境界線は、リポジトリの設定ファイルを開けば数行で確認できます。

10の結果は何なのか

READMEに列挙されている10件と、対応するLeanモジュール名は次のとおりです（openai/ten-proofs README）。

  1. 高次元球充填──Cohn–Elkies閾値に到達する漸近上界の改善（SpherePacking.lean）
  2. 二元符号・球面符号──あらゆる最小距離において指数的に強い上界（MetricCodes.lean）
  3. 非ソフィック群──すべての群が有限置換近似を持つかという問題の解決（NonSoficGroup.lean）
  4. Connesの剛性予想──群フォンノイマン環が群を決定するという予想への反例（ConnesRigidity.lean）
  5. 算術回路計算量──permanentに対する $n^4/\log n$ のformula下界を含む新しい下界（Permanent.lean）
  6. 量子並列反復──任意の有限2人量子ゲームに対する指数的並列反復定理（QuantumParallelRepetition.lean）
  7. 最近ベクトル問題──多項式因子の近似困難性と格子への帰結（GapCVP.lean）
  8. Ehrhartの体積予想──各次元における鋭い最大体積（EhrhartVolumeInequality.lean）
  9. 多色Ramsey数──Erdős問題183を解決する超指数下界（MulticolorTriangleRamsey.lean）
  10. 極値グラフ理論──Erdős問題146と180を解決する反例（CompactnessAndDegeneracy.lean）

分野的な広がりが目を引きます。作用素環論（Connes剛性）、幾何学（球充填、Ehrhart）、群論（非ソフィック群）、量子計算量、格子暗号（CVP）、極値組合せ論が一つのリリースに同居しています。

球充填については、高次元での一般的な上界の指数が1978年の Kabatiansky–Levenshtein 以来更新されていませんでした。その古典的な形は

$$\Delta_{\mathbb{R}^n} \le 2^{-(0.5990\ldots + o(1))n}$$

というもので、今回の結果は Cohn–Elkies の線形計画限界の厳密な漸近レートを決定することで、この指数を1978年以来はじめて動かしたと説明されています（implicator.ai）。

非ソフィック群のほうは、soficityの概念が1999年に導入されて以来27年、非ソフィック群が存在するかどうかが未決着でした（implicator.ai）。ここで「明示的な構成が出た」という主張は、群論の側から見ればかなり大きな話になります。

Lean証明書は何を保証するのか──comparatorと3つの公理

ここが今回の技術的な核心です。「Leanで検証済み」という言葉は、実は複数の異なる強さを持ちえます。よくある抜け道は3つあります。

  • 証明の途中に sorry を残す（未完成部分を穴として通す）
  • 独自の公理を追加宣言する（定理を定義によって真にしてしまう）
  • 形式化した命題が、実は元の未解決問題より弱い／別物である

このリポジトリが面白いのは、これらのうち前2つを機械的に潰す仕組みを同梱している点です。lakefile.toml は mathlib に加えて leanprover 公式の Comparator v4.32.0 に依存しており、ComparatorChallenges/ ディレクトリに12個の設定ファイルが置かれています（READMEの10結果に対して12個なのは、二元符号と球面符号、およびcompactness予想と2-degenerateグラフがそれぞれ分割されているためです）。

球充填の設定ファイルの中身はこうなっています（openai/ten-proofs A_SpherePacking.json）。

{
  "challenge_module": "ComparatorChallenges.A_SpherePacking",
  "solution_module": "SpherePacking",
  "theorem_names": [
    "PackingBounds.FullMain.exact_limit",
    "PackingBounds.FullMain.exact_binary_exponent",
    "PackingBounds.PackingBridge.sphere_packing_sharp_asymptotic_upper",
    "PackingBounds.sharpFullCohnElkiesManuscriptConclusions"
  ],
  "permitted_axioms": [
    "propext",
    "Quot.sound",
    "Classical.choice"
  ],
  "enable_nanoda": true
}

permitted_axioms に並ぶ3つは、Leanにおける標準の基礎公理そのものです。命題外延性、商型の健全性、選択公理──これ以外の公理が証明に混入していればcomparatorが弾きます。非ソフィック群の設定ファイル D_NonSoficGroup.json も同じ3公理のみを許可し、検証対象の定理として SoficGroups.SourceTopLevelCompressionFinal.exists_finitelyPresented_nonsofic_group を名指ししています。

さらに enable_nanoda: true が効いています。comparator 自身が外部バイナリとして呼び出すのは landrun（サンドボックス）、lean4export（oleanのエクスポート）、そして nanoda_bin（独立カーネル、enable_nanoda が真のときのみ必要）の3つです（leanprover/comparator）。lean-evalのドキュメントはこの検証パイプラインを landrun / lean4export / comparator / nanoda の4ツールの組み合わせとして説明しており、nanoda が提出された証明を独立に再生します（leanprover/lean-eval）。つまりLean本体のカーネルとは別実装のチェッカーがもう一度型検査を回す構成です。

実行には事前準備が要ります。公式READMEは landrun・lean4export・nanoda_bin（独立カーネル検査を使う場合）をあらかじめビルドして PATH に通しておくよう求めており（openai/ten-proofs ComparatorChallenges README）、単にリポジトリを clone してビルドコマンドを叩くだけでは終わりません。その準備を済ませれば、リポジトリのルートから次の2行でcomparatorを実行できます（leanprover/comparator）。

lake exe cache get
lake exe comparator ComparatorChallenges/A_SpherePacking.json

comparatorの設計思想は、証明の実装と仕様の分離にあります。ベンチマーク側が短く人間可読な命題を Challenge.lean に一度だけ書き、提出物がその命題を「ちょうど」証明していることを機械的に照合する。lean-evalの説明では、comparatorが通ることで、提出された証明が宣言された命題そのものを証明し、3つの基礎公理のみに依存し、Leanカーネルに受理されることが保証されるとされています（leanprover/lean-eval）。

ただしこの保証には前提があります。comparator自身のREADMEは、Challenge側のインポートや lakefile.toml、OS・ハードウェア、サンドボックス機構である landrun、そしてLeanまたはnanodaの少なくとも一方のカーネルを信頼基盤として挙げています（leanprover/comparator）。さらに、命題を未定義のまま残す「definition hole」形式のチャレンジについては、追加の監督なしにゲーム化されうるとし、その種の解答は必ず人間を含む追加の検証者によって確認されるべきだと明記しています（leanprover/comparator）。今回の12設定がdefinition holeをどの程度使っているかまでは公開情報から確認できていません。

第三者が手を動かして確かめられる範囲としては、これは相当に高い水準です。ただし「独立カーネルまで含めた検証手順」であって、無条件・無前提の検証ではありません。

証明書の外側に残るもの

一方で、上の3つの抜け道のうち3番目は原理的にcomparatorでは潰せません。形式化された命題が、数学者が10年以上取り組んできた元の問題と本当に同じことを言っているかどうかは、人間が Challenge.lean を読んで判断するしかないからです。

この点は複数の媒体が指摘しています。Leanの検証は形式的証明の妥当性を確認するが、その形式的命題が数学者の意図した未解決問題と一致しているかは検証しない、という整理です（BitsMinds 2026-08-01）。球充填の設定ファイルに sharpFullCohnElkiesManuscriptConclusions という定理名があることは、逆に言えば「manuscriptの結論に対応する命題」が形式化のどこに置かれているかを読み解く作業が読者側に残ることを意味します。

もう一つ、証明書がまったくカバーしないのが生成プロセスです。OpenAIの説明によれば、モデルが中核の議論を出し、人間の研究者が同じモデルを使って論文の形に整え、モデルが各結果をLeanに形式化した、という流れです（Developers Digest）。この「人間が整えた」部分がどれだけの分量だったのか、各問題に何回試行したのか、どれだけの候補から選抜したのかは公開情報からは読み取れません。

OpenAI自身の研究者もそこは限定的に語っています。Noam Brown氏はXへの投稿で「他の主要問題も試したが成功しなかった。残念ながらミレニアム懸賞問題はまだだ。ただし各問題に多くを費やしたわけでもない。テスト時計算量はもっと押し上げられる」と述べています（@polynoamial）。10件の成功の背後に何件の失敗があったかは、この投稿以上には示されていません。

数学者側の反応としては、マンチェスター大学のThomas Bloom氏（erdosproblems.comの運営者）が「big news」と評価し、OpenAIが以前に出した単位距離問題の反例より数学的に大きいと述べています（implicator.ai）。ただし発表からまだ日が浅く、外部の数学者がこの種の予想に通常かけるだけの深さで議論を追い切る時間は経っていません。

約2,000ドルという数字の読み方

解の探索に要したトークンが Sol API レートで約2,000ドル相当という数字は、報じ方によって意味が変わります。

「10件の未解決問題が20万円で解けた」と読むこともできますが、この金額に含まれていないものを数えたほうが有益です。含まれていないのは、Astra自体の訓練コスト、問題選定にかけた人間の時間、失敗した試行の分（Brown氏が言及した「成功しなかった他の主要問題」）、論文249ページへの整形、そしてLean形式化を通すまでの反復です。形式化には一般に追加の作業を要しますが、今回の形式化に投じた人員・計算量・期間は公開されていません。

それでも、この数字が示唆するものはあります。Developers Digestは、この水準なら資金のある研究室ならどこでも手が届くと評しています（Developers Digest）。ただし前提として、Astra は未公開の内部モデルです。リポジトリを clone して lake build All を回すことは誰でもできますが、Astra に別の問題を投げることは現時点では誰にもできません（implicator.ai）。

Astraそのものについては、数時間から数日にわたる問題解決を想定したモデルファミリーとされ、GPT-6として出るのかGPT-5系の派生になるのかは未定、公開日も示されていません。Sam Altman氏がワシントンの政策担当者にデモを行い、米政府の事前審査を受ける最初のモデルになるとも報じられています（the-decoder 2026-08-01）。

Leiden Declarationとの衝突

今回の発表は、数学コミュニティ側の動きと正面からぶつかる位置にあります。

2026年6月2日、15大学の研究者らが Leiden Declaration on Artificial Intelligence and Mathematics のプレスリリースを出しました（Leiden Declaration）。国際数学連合が支持するこの宣言は、AI生成の証明への依存が数学研究の正確性・信頼性・独立検証可能性を脅かすこと、技術企業の関与拡大が研究の優先順位をAIに扱いやすい問題へ歪めうること、そしてAIにアクセスできない研究者が不利になることを警告しています。宣言は、数学の結果は査読を経た媒体でオープンサイエンスの原則のもとに公表されるべきであり、「理解するために専有的な知識や機材を要求すべきではない」としています。

OpenAIのリリースは、この最後の点に対して部分的な回答になっています。証明書を公開し、独立カーネルまで含めた検証手順を同梱したことは、独立検証可能性の要求に真正面から応えた形です。しかし査読を経ていないプレスリリース先行という形式自体は宣言が名指しで批判した構造そのものです。開示の面では、Astraの関与とトークンコストの概算は今回のリリースで示された一方、モデル本体へのアクセス・訓練データ・外部が試せる公開テスト用インターフェースは提供されていません（implicator.ai）。

著者性についても OpenAI は今回の発表で Leiden Declaration に言及し、「完全にAIが生成した証明に人間の著者性を主張することは、システムの貢献と人間の真の知的営為の性質の双方を誤って表現することになる」という立場を示しています。中核となる数学的議論はシステム自身から出たもので、OpenAI側は原稿の作成とLeanでの形式化を助け、その正しさに責任を負う、という整理です（the-decoder 2026-08-01）。

なお、OpenAIは今回の発表とは別に「ChatGPT for Academic Researchers」プログラムを通じ、2027年にかけて10万人の研究者へフロンティアモデルを無償提供する計画を発表しています（今夏1万人から開始し段階的に拡大、対象は数学者に限らず科学者・エンジニアを含みます）。ただしこれはAstraそのものへのアクセスではなく、現時点で提供対象と明示されているのはGPT-5.6系モデルです（OpenAI 2026-07-29）。

残された不確実性

  • 形式化命題と元の問題の一致: comparatorは提出された証明が Challenge.lean の命題を証明することを保証しますが、その命題が数学者の考える未解決問題と等価かは人間の判読に委ねられます。10件それぞれについて、この照合作業はまだ外部で完了していません。
  • 公式ページの直接確認: 本記事の執筆時点で openai.com/index/ten-advances-in-mathematics/ への直接アクセスは403が返るため、公式ページの記述は複数の独立媒体が同URLを一次情報として引用した内容に依拠しています。リポジトリの内容は直接確認しました。
  • 試行回数と選抜の度合い: 何回の試行から10件が選ばれたのか、人間がどこまで問題を切り出して与えたのかは開示されていません。Brown氏の投稿は失敗の存在を認めていますが、規模は不明です。
  • 査読の不在: 現時点で249ページの論文が査読済み媒体に掲載されたことは確認できません。Leanが通ることと、数学コミュニティが結果を受け入れることは別の工程です。
  • モデルの再現性: Astraは未公開で、外部の第三者が同じ問題に同じモデルを投げて追試することはできません。証明書は再現可能ですが、生成プロセスは再現できません。
  • 未解決期間という指標の読み方: BitsMindsは、問題が本当に難しかったのか、単に注目されてこなかったのかの区別が明確でないと指摘しています（BitsMinds 2026-08-01）。分野ごとに未解決の重みは異なります。

まとめ

今回のリリースで確実に言えるのは、次の3点です。

第一に、検証の水準が明確に上がりました。permitted_axioms を propext / Quot.sound / Classical.choice の3つに限定し、独立カーネル nanoda での再生を有効にした設定ファイルが公開されている以上、指定された定理本体について「隠れた公理で真にしている」「sorry で穴を空けている」という疑いは、landrun / lean4export / nanoda_bin を整えたうえでcomparatorを回せば機械的に潰せます（definition holeを使うチャレンジ設計自体の妥当性は別途人間の確認が要ります）。2026年5月のErdős問題の結果が名指しの数学者による人手レビューに依拠していたことと比べると、検証の性質が変わりました（BitsMinds 2026-08-01）。

第二に、証明書が保証する範囲は依然として狭いままです。保証されるのは「宣言された命題が3公理のみで証明されている」ことであって、「その命題が問題として意味がある」ことでも「AIが人間の助けなしにそこへ到達した」ことでもありません。後者2つを判定するには、Challenge.lean を読む数学者と、生成プロセスの開示が要ります。

第三に、この2つのギャップこそが Leiden Declaration が問題にしている場所と重なっています。形式化証明書は独立検証可能性という論点に対する強い回答ですが、査読・開示・アクセスという残りの論点には触れていません。

読者として取れる態度は、見出しを丸ごと信じることでも一蹴することでもなく、ComparatorChallenges/*.json を開いて何が許可され何が検証されているかを自分で読むことだと思います。今回のリリースは、少なくともそれが可能な形で出されています。

主要出典

関連する過去記事