Astraとは何か — 現時点で分かっていること

Astraは未公開で、判明している情報は限られています。

位置付け：OpenAIの次世代主力モデル群です。既存のSol、Terra、Lunaと並ぶ新しいモデルクラスとされています。最終的にGPT-6と呼ばれるのか、GPT-5.7のような番号になるのかは未定で、公開日も決まっていません。

中核能力：複数のエージェントを連携させ、数時間から数日間にわたって動かし、極めて複雑な長い推論問題に取り組むよう設計されています。OpenAIが挙げる用途は、複雑なプロジェクトと高度な数学です。Sam Altmanはすでにワシントンで、政治家や規制当局者にデモを行ったとされています。

未解決の弱点：長時間の処理では誤りが蓄積します。途中で方向を誤った場合に自力で修正できるかも、現在のシステムに共通する既知の弱点であり、まだ克服されていません。密接に結合したタスクでは、複数のエージェントを使うことで調整コストが増え、単独のエージェントより悪化する場合もあります。Astraがこの課題をどこまで解決したかを示す公開証拠はありません。今回の数学10件が、唯一公開された成績表です。

上記の「位置付け」と「中核能力」は、3人の関係者を引用したThe Informationの報道に基づき、本サイトはThe Decoder経由で確認しました。OpenAIの公式発表ではありません。公式に確認できるのは次の点だけです。発表本文には「Astra」という名前が一度も登場せず、「次期主力モデルの内部版」とだけ書かれています。Astraという名称を明かしたのは、発表当日にXへ投稿したOpenAI研究者のNoam Brownです。

10件の成果一覧

何の記録を破ったのか、表でまとめます。

「停滞期間」は249ページの論文の各章序文とErdős Problemsを本サイトが項目ごとに照合したものです。極値組合せ論の2行を合わせて、公式発表における10番目の成果に当たります。このため、表の10行が10件の成果に対応します。

必要な数学的アプローチは3種類に分けられます。第1は、数十年動かなかった境界を更新すること。第2は、ある対象が計算可能か、突破可能かを判定すること。第3は、反例をゼロから構成して予想そのものを覆すことです。

より密に詰める――数十年ぶりの上界更新

タイプ1の3題は、同じ問いを扱います。制約された空間に、最大でどれだけ多くのものを詰め込めるかです。

計算可能性と突破の限界を見極める

タイプ2では焦点が変わります。どれだけ詰め込めるかではなく、そもそも計算できるのか、突破できるのかを判定します。計算機科学や暗号に最も近い領域です。

パーマネント：行列式との差は符号1つ、難しさは別次元

ここでいうpermanentはパーマネントです。行列積ではありません。中国語の要約ではしばしば誤訳されています。

n人をn個の職務に割り当て、各人と各職務の相性に点数があるとします。「1人1職務、1職務1人」となるすべての割り当てを列挙します。各割り当てではn個の点数を掛け、すべての割り当ての値を足し合わせます。これがパーマネントです。行列式も式は同じですが、割り当ての半分に負号を付ける点だけが違います。

符号を半分取り除くだけで、同じ式が「瞬時に計算できる」ものから「計算不能」に変わります。なぜそうなるのかは、今も分かっていません。Valiantは1979年、パーマネントがVNP完全問題であると証明しました。多数の計数問題の頂点に位置するという意味です。パーマネントを計算する多項式サイズの式が見つかれば、代数的複雑性理論の広い範囲が崩れます。代数の世界におけるP対NP問題です。

もちろん、最大の難問そのものが解決したわけではありません。今回は「最低でもどれほど大きくなければならないか」という下界を引き上げました。除算なしの算術回路には少なくともΩ(n²·log log n)個のゲートが必要です。算術式には少なくともΩ(n⁴/log n)個の葉が必要で、後者は分母が恒等的にゼロでない限り、除算を認めても成立します。この種の下界は、最大の難問を反対側から追い詰める唯一の手段です。下界が上がるたびに、「実は簡単に計算できる」という可能性が狭まります。

未知の反例をゼロから構成

真に難しいのはタイプ3です。前の2類では、すでに引かれた線を先へ進めます。方向は明確です。しかし、この類では無から有を生む必要があります。誰も見たことのない数学的対象を頭の中で組み立て、それが実在し、互いに衝突する複数の条件を同時に満たすと証明します。4件がこの類に属し、そのうち3件は数十年来の予想を直接覆しました。

10件の成果から見えるモデルの実力

10件を並べると、何が読み取れるでしょうか。以下は誇張ではなく、ここまでに示した事実から読み取れる点です。

信頼の根拠 — 47万行の証明を機械が行単位で検査

AIが数学的成果を主張すること自体は、すでにニュースではありません。従来の論争は常に同じ場所で止まりました。誰が査読し、読み切れるのか。今回は論理検証を機械に委ねました。10件の証明をすべてLeanで書き直し、行単位の検査を終え、コードも公開しています。

Leanは定理証明支援系です。数学的証明をLeanの言語で書き直すと、最小限のカーネルが行ごとに検査します。各ステップが、それ以前のステップと公理から厳密に導かれているかを確認します。検査を通れば、その形式化された証明に論理上の穴がないことを意味します。

帳簿を調べる監査人に似ています。監査人は事業内容を理解する必要がありません。すべての入出金の計算が合っているか、証憑があるかだけを確認します。合わなければ、商業的にどれほど妥当でも差し戻します。Leanも同じです。フォン・ノイマン環を理解しているわけではなく、各推論が規則に合っているかだけを確認します。数学の証明は従来、専門家が1行ずつ読む必要がありました。しかし10分野すべてを読める人はほとんどいません。これが「AIによる数学」が従来必ず行き詰まった場所です。

本サイトでは、リポジトリをクローンし、実際に数えました。47万行を1行1秒で休まず読んでも、5日半かかります。実測値は次の通りです。

sorryはLeanのプレースホルダーで、「この手順はひとまず飛ばす」という意味です。証明内に1つでもあれば穴があります。リポジトリ全体に1つもありません。

公理（axiom）は、推論体系の最下層にある、それ以上証明しない出発点です。Lean標準ではpropext、Classical.choice、Quot.soundの3つだけです。独自の第4公理を密かに追加すれば、途中で規則を変えたことになり、結論は有効とはいえません。10件の証明が使うのは標準の3つだけで、各成果の検証設定には許可する公理が個別に明記されています。

リポジトリには独立した再検査経路もあります。Comparatorとnanodaです。nanodaはLean公式カーネルとは別に実装された型検査器です。Lean自体を信頼せず、独立実装のカーネルで再検査できます。

機械が保証できない両端、そして著者表記を巡る対立

機械が保証できるのは中央部分だけです。検証チェーンの両端は、まだ空いています。

濃色 = 完了した2段階

入口：翻訳の正しさは機械の保証外

数十年間自然言語で記述されてきた予想を、Leanの形式命題へ翻訳する作業は、人間またはAIが行います。翻訳時に命題が密かに弱められたり、定義がずれたりしても、Leanは合格を出します。Leanが担うのは命題から結論までの推論であり、その命題が数学者の意図した問題と同じかどうかは判断しません。

OpenAIはこの確認に備えています。リポジトリのComparatorChallengesディレクトリでは、各成果について検証対象の定理名を個別に列挙しています。Ramseyの項目なら、ErdosProblems.MulticolourTriangleRamsey.erdos_183など4本です。「証明したと主張する命題はこれだ」と公開し、人間が確認できるようにしています。ただし、公開されていることと、誰かが確認済みであることは別です。

出口：レビュー状態は「AIによるレビュー」

リポジトリ直下のformalization.yaml末尾には、発表文で触れられていない1行があります。

review:
  status: "agent-reviewed"

つまり、形式化のレビュー状態はagent-reviewedです。人間ではなくAIによるレビューです。249ページの論文も査読前で、著者欄には人名がなく「OpenAI」とだけ書かれています。検証チェーンの最後の段階は、現時点で空いています。

公開された「思考過程」は思考連鎖そのものではない

発表では、各解についてモデル自身が思考過程を説明した文書を公開したとしています。この表現は、元の思考連鎖が公開されたように読めます。しかし62ページの文書は、概要で作成経緯を説明しています。AIモデルが元の思考連鎖と最終論文を読み、証明がどのように形成されたかを再構成したものです。モデルの実際の推論を研究する資料としては、間に1層挟まっています。

最大の対立点は著者表記

ここでは判断を加える必要はありません。2つの文書を並べれば、違いは明確です。

OpenAIは同じ発表文で、ライデン宣言の署名者に「深い敬意と理解」を示しています。同宣言の価値観に関する節には、成果は具体的な著者へ帰属させ、発見の功績と正しさへの責任を著者が負うべきだとも書かれています。今回の249ページの論文には、人間の著者名がありません。

公平を期せば、宣言の別の提言である「ツール使用の開示」は、OpenAIも実行しています。モデル、費用、形式化の過程を公開しました。

登録サイト管理者は評価、しかし登録はOPENのまま

Erdős Problems（erdosproblems.com）は、マンチェスター大学の数学者Thomas Bloomが運営しています。この分野における事実上の権威ある索引であり、OpenAIの249ページの論文も参考文献で引用しています。

発表当日、Bloom本人がXに投稿しました。

大ニュースです！（実際には私の専門ではありませんが、そうですね、単位距離予想の反例より上に置きます。単位距離予想そのものを証明するほどではないかもしれませんが、構成という点では大きな成果です。）

Thomas Bloom · X · 2026-08-01

「単位距離予想の反例」とは、OpenAIが今年5月に公開した成果です。未公開モデルを使い、Erdősの単位距離予想を覆しました。Bloomは今回の10件をその上に置きました。理由は「構成という点」です。本稿のタイプ3に当たる、対象をゼロから作る作業を指します。

10分後、Bloomはさらに投稿し、これをAIによる数学者の代替と表現する見方に反論しました。

数学者が提起した予想を、数学者が1世紀以上かけて発展させた理論を使い、数学者が作り、数学者のあらゆる著作を学習したAIで証明して、それを「数学者の代替」と呼ぶのは正しくありません。

Thomas Bloom · X · 2026-08-01

ただし評価とは別に、登録サイトの状態は変わっていません。本サイトが2026年8月2日に3件を再確認した結果は次の通りです。

3項目とも未解決の表示が残り、「コメントには部分解、完全解を問わず、解を主張する投稿はない」と記されています。

この2点は分けて考える必要があります。管理者による公開評価と、登録サイトが項目ごとに検証して反映することは別です。Bloom自身も「専門ではない」と断っています。彼が示したのは熟練数学者としての成果の重みに対する評価であり、証明の各手順を検証した結果ではありません。検証を完了するには、専門家が数十ページの論文を読み、数万行のLeanコードにある命題宣言を確認し、その形式命題が元の問題と一致すると確かめる必要があります。数日では終わりません。

分野の権威ある研究者は成果の重要性を公に認めました。一方、10件のうち独立検証を完了したものはまだありません。

最難関には届かず、公開前には政府審査も

この先はどう進むのでしょうか。発表文にない3つの手掛かりがあります。

さらに難しい問題にも挑戦したが、失敗

Noam Brownは発表当日、本文になかった事実を補足しました。

はい、他の重大問題にも実際に挑戦しましたが、成功しませんでした。残念ながら、ミレニアム懸賞問題はまだありません。
ただし、各問題に使った計算資源は多くありません。テスト時の計算資源は、さらに大幅に増やせます。

Noam Brown · X · 2026-08-01

ミレニアム懸賞問題は、Clay Mathematics Instituteが2000年に設定した7つの問題です。各問題に100万ドルの賞金があります。26年間で解決されたのは1題だけです。

この発言を先ほどの2000ドルと合わせると、意味は明確です。今回の10題は、計算資源をあまり投入せずに達成しました。しかし本格的に投入したとき、最上位の問題へ届くかは誰にも分かりません。BrownはAstraを「科学的推論における大きな一歩」と表現しました。

政府審査を受ける最初のモデルに

The Informationの報道によると、Astraはすでにテスト中です。米政府の新しいAI審査枠組みの対象となる最初のモデル群に入る見込みで、公開前に連邦政府へ提出する必要があります。枠組み自体はまだ策定中です。

読者にとって重要なのは、今回の数学10件が能力の実演であると同時に、モデルが公式審査を控える時期に発表されたことです。本サイトは動機を判断せず、時間的な関係だけを示します。

さらに先の目標：自律的に研究するAI

報道では2つの時期が示されています。OpenAIは2028年3月までに、研究プロジェクトを独力で進められる完全自動のAI研究者を作ることを目指しています。より近い目標は今年9月です。「研究インターン水準」のシステムを投入し、人間の科学者を支援する計画です。

今回の数学10件は、そのロードマップで現時点までに提出された唯一の具体的成果です。機械が論理を完全検証できる分野では、この仕組みが実際の成果を生み出せると示しました。一方、形式検証できない分野でも同じ方法が成立するとは証明していません。研究の大半は、まさに後者に属します。

検証用リンクとコマンド

著者表記を巡る論争について、両者の主張を聞くだけで済ませる必要はありません。資料はすべて公開されています。ただし、249ページの論文と62ページのウォークスルーには、発表本文からリンクされていません。GitHubリポジトリのREADMEから探す必要があります。

lake exe cache get
lake build All

# 只验其中一个（球堆积），走第三方内核
lake exe comparator ComparatorChallenges/A_SpherePacking.json

10題で求められる数学的作業は同じではありません。3種類に分けると、モデルの強みが見えてきます。

AIによる数学的成果の主張は以前からあります。論争は常に同じ点で止まりました。誰が査読し、読み切れるのか。今回は論理検証を機械に委ねました。

Leanは定理証明支援系です。証明をLeanの言語で書き直すと、最小限のカーネルが各手順を行単位で確認します。それまでの手順と公理から厳密に導かれているかを調べるのです。帳簿を調べる監査人に似ています。事業内容を理解する必要はなく、各項目が正しいかだけを確認します。10件の証明はすべてLeanで書き直され、行単位の検査を終え、コードも公開されています。

sorryはLeanのプレースホルダーで、「この手順は飛ばす」という意味です。1つでもあれば証明に穴があります。公理は推論の最下層にある出発点で、1つ追加すれば途中で規則を変えたことになります。リポジトリには再検査経路もあり、Leanのカーネルを信用しない場合は、別実装のカーネルで再検査できます。

機械が保証できるのは中央部分だけです。チェーンの両端はまだ空いています。

論理検査を機械へ任せたことで、論争は別の問いに集中しました。この証明は誰の名前で発表すべきなのか。

ライデン宣言の別の提言であるツール使用の開示は、OpenAIも実行しました。モデル、費用、形式化の過程を公開しています。