Astra

何が起きたのか OpenAIが2026年8月7日、公式Xで次期モデル「Astra」について次のように投稿しました。「After evaluating one of our upcoming models, Astra, we’re treating it as our first “critical” model for cybersecurity under our Preparedness Framework.」（OpenAI公式X 2026-08-07）。同時に公式ブログ『Responding to the next frontier of critical cyber capabilities』が公開され、追加の管理策が列挙されました（OpenAI 2026-08-07）。 ただし公式ブログ本文の表現は「Critical と判定した」ではありません。厳密には「we cannot rule out Critical capability level at this time」——現時点で Critical 能力レベルを排除できない——であり、しかもその根拠は予備評価（preliminary evaluations）の段階だと明記されています（TechCrunch 2026-08-07）。運用上は初のサイバー Critical 相当として扱う一方、Critical 閾値を超えたと確定させたわけではない、という二段構えです。 Preparedness Framework は OpenAI が2023年12月に公表し、v2を2025年4月15日に更新した社内の安全枠組みです。追跡対象は Biological and Chemical / Cybersecurity / AI Self-improvement の3領域で、それぞれに High と Critical の2段階の能力閾値が定義されています（Preparedness Framework v2 PDF）。 ...

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