OpenAI Astraとは何か
Astra とは、OpenAI が「次の主要モデル」と表現しているモデルです。今回の成果を出したのは、そのうち社内版にあたるもので、一般には提供されていません。公表されたのは成果物であって、モデルそのものではありません。
今回の公表の基本情報
Today, we are sharing a selection of ten results, each of which resolves or makes substantial progress on a long-standing open problem. ／ The results were achieved by an internal version of Astra, our next major model. The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates. These arguments were then prepared into manuscripts by humans with the same model. Afterward, the model formalized each argument in a Lean certificate ／ We are also releasing for each solution a model's narration of its thinking process. — 導入段落および "The results" 節の、成果の位置づけ・探索に要した費用・公開物に関する記述より
解かれた10問題は分野をまたいでいる
内訳を見ると、1つの得意分野に偏っていません。高次元幾何・符号理論・算術回路計算量・群論・作用素環・量子計算量・格子暗号・極値組合せ論にまたがっています。
10件の成果（公式の一覧より抜粋して整理）
| 問題 | 得られた結果 |
|---|---|
| 高次元の球充填 | 充填密度の上界を Cohn–Elkies の閾値まで改善 |
| 2進符号・球面符号 | 最小距離を指定したときの符号の最大サイズについて指数的に強い上界 |
| 非 sofic 群 | 非 sofic 群の存在を示す構成。群論の中心的な未解決問題に答えるもの |
| Connes の剛性予想 | 群がその von Neumann 環で一意に決まるという予想の反証 |
| 算術回路計算量 | パーマネントの計算について新しい下界。算術式では n⁴/log n の下界 |
| 量子並列反復 | 一般の2人量子ゲームに対する指数的な並列反復定理 |
| 最近ベクトル問題 | 多項式因子の近似困難性。耐量子暗号に関わる格子の基礎問題 |
| Ehrhart の体積予想 | 内部格子点が重心のみである凸体の最大体積を全次元で決定 |
| 多色 Ramsey 数 | 多色三角形 Ramsey 数の超指数的な下界（Erdős 問題183を解決） |
| 極値数の予想 | 極値グラフ理論のコンパクト性予想と退化性予想（Erdős 問題146・180を解決） |
These problems span high-dimensional geometry, coding theory, arithmetic circuit complexity, group theory, operator algebras, quantum complexity, lattice cryptography and extremal combinatorics. ／ Non-sofic groups. A construction establishing the existence of non-sofic groups, addressing a central open question in group theory. ／ Connes's rigidity conjecture. Disproof of a longstanding conjecture that certain groups are uniquely determined by their von Neumann algebras. ／ Multicolor Ramsey numbers. A superexponential lower bound for multicolor triangle Ramsey numbers, resolving Erdős problem 183. ／ Extremal number conjectures. Results on the compactness and degeneracy conjectures in extremal graph theory, resolving Erdős problems 146 and 180. — 対象分野の列挙、および表に挙げた成果のうち非sofic群・Connesの剛性予想・多色Ramsey数・極値数の予想の4件の記述より（残る6件も同じ一覧に併記されている）
5月の反証から続く流れにある
今回が突然出てきたわけではありません。OpenAIは2026年5月にも、未公開モデルの評価中に見つかったという Erdős の単位距離予想の反証を公表しています。公式は、この成果がすでに数学と理論計算機科学のその後の発展につながったとし、脚注で5本の後続論文を挙げています。
背景には研究者への提供拡大もあります。同社は ChatGPT for Academic Researchers として、10万人の科学者・数学者へ最上位モデルを無償で開放する取り組みを進めており、その延長で開発中のモデルを未解決問題にかけ続けている、という説明になっています。この取り組みについてはOpenAIが研究者10万人へ無償提供する件でも扱っています。
That is why we recently announced ChatGPT for Academic Researchers, an initiative providing 100,000 scientists and mathematicians with free access to our best ChatGPT models. We also continue to evaluate our models on open research problems during development. ／ In May, we shared an AI-generated disproof of the Erdős unit-distance conjecture, discovered while evaluating an unreleased model. This work has already inspired further developments in mathematics and theoretical computer science ／ Subsequent research includes Bloom, Sawin, Schildkraut, and Zhelezov, "The sum-product conjecture is false for real numbers"; Pohoata, "Split primes and the Elekes-Rónyai problem"; Saha, Xu, and Ye, "Furthest Pair Requires Quadratic Time in Superconstant Dimension under SETH"; Goh and Hatami, "Communication complexity of point-line incidences over the reals"; and Lee, Pohoata, and Zhu, "The Minkowski grid has robustly many repeated distances." — 研究者向けの提供、5月の反証からの流れ、および脚注に挙げられた後続研究5本より
証明はLeanで機械検証されている
この公表がこれまでと違うのは、主張だけでなく機械検証できる形の証明が付いていることです。ここは実際に確認できるので、公開されたものを取得して中身を見ました。
公開されたLean証明の実測（2026年8月4日・編集部が公開リポジトリの main ブランチ 94bc0fe を取得して集計）
| 項目 | 実測値 |
|---|---|
| 本体の形式化ファイル | 10本（成果1件につき1ファイル） |
| 本体10本の行数合計 | 548,215行 |
本体10本の未証明の穴（sorry） | 0件 |
本体10本の追加公理（axiom） | 0件 |
| ライセンス | Apache License 2.0 |
| 使用環境 | Lean 4.32.0／mathlib（Lean の標準数学ライブラリ）／Lake（Lean のビルドツール） |
This repository contains Lean 4 formalizations of the results presented in ／ The project uses Lean 4.32.0, mathlib, and Lake. ／ Apache License — 公開リポジトリの位置づけ、ビルド環境、およびライセンス表記より
未証明の穴も追加の公理も無かった
形式化された証明を読むとき、まず見るのは2点です。1つは sorry（未証明の箇所を示す印）が残っていないか。もう1つは axiom（証明せずに前提として置く命題）が勝手に足されていないかです。都合の悪い部分を公理として置いてしまえば、どんな主張でも「証明」できてしまうためです。
公開リポジトリを取得して10本の本体ファイルを機械的に数えたところ、sorry も axiom も1件もありませんでした。行数の合計は548,215行に達します。人が書いたものではない量です。
ここで注意が要ります。リポジトリ全体で sorry がゼロというわけではありません。独立検証用の課題ファイルを収めた別ディレクトリには sorry が42箇所あります。ただしこれは埋め残しではなく、後述する第三者検証のために意図的にそうなっている部分です。二次情報で「リポジトリに sorry はゼロ」とだけ読むと、この区別を落とします。
第三者が独立に検証するための課題も同梱されている
もう1つ見落とせないのが、別実装の検証器で突き合わせるための仕組みが最初から入っていることです。リポジトリには Comparator という照合ツール向けの課題ファイルが同梱され、その手順書は landrun・lean4export・nanoda_bin を用意するよう指示しています。
この nanoda（ナノダ）は、Lean 公式カーネルとは別に Rust で書かれた独立実装の検証器です。OpenAI 側が、自分たちの証明を他人の実装で検証させる導線を用意しているという構図になります。しかも同じ週に、その nanoda 自身のバグが問題になる出来事も起きていました。詳しくはコラッツ予想のAI「反証」がなぜ無効だったかをご覧ください。公開された証明ファイルを手元の版と突き合わせて確かめるなら、差分を並べて読むところから始められます。
無料ツールテキスト差分比較2つのテキストの差分をハイライト表示。変更点を素早く発見できます。今すぐ使ってみる →
For instructions on checking the formalizations with Comparator, see the…／Install `landrun`, `lean4export`, and `nanoda_bin`, and make them available on `PATH`. — 独立検証の案内、および Comparator 用課題の手順書より
nanoda is an independent kernel (aka proof/type checker) for Lean implemented in Rust by Chris Bailey . ／ The original Collatz repository also passed a week-old version of nanoda , the main external checker. — nanoda が Rust による独立実装の検証器である点、および同時期にその nanoda 側でも問題が起きていた点の根拠として
著者性についてOpenAIが示した立場
技術的な成果と並んで注目されたのが、成果を誰の功績とするかについての表明です。AIが生成した証明を人間の論文として出してよいのか、という問いに正面から答えています。
人間の著者性を主張しない
OpenAIの立場は明確です。AIシステムが全面的に生成した証明について人間の著者性を主張することは、システムの寄与と、人間の本当の知的作業の両方を偽ることになるとしています。帰属は、その成果が実際にどう生み出されたかを正直に反映すべきだ、という原則です。
そのうえで役割分担を書き分けています。論文への整形と Lean での形式化は OpenAI 側が手伝い、その正しさについては同社が責任を負う。一方で数学的な論証そのものはシステムが生成したものである、という切り分けです。AIを使った成果の書き方として、ひとつの参照点になります。
We believe attribution should honestly reflect how a result was produced: claiming human authorship for a proof generated entirely by an AI system would misrepresent both the system's contribution and the nature of genuine human intellectual work. We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness, while the mathematical arguments themselves were generated by our system. — 著者性と責任の所在に関する記述より
懸念する側への言及も置いている
同社は、AIが数学研究に寄与できるようになったことが技術企業だけでは答えられない問いを生むと書いています。そのうえで、AIと数学に関する Leiden 宣言の署名者を含め、影響を懸念する人々に敬意と理解を持つと述べています。
数学コミュニティに対しては、成果を深く検討し、文脈の中に位置づけ、そこにある発想を新しい研究へつなげてほしいと呼びかけています。成果を投げて終わりにしない姿勢を、公表の中に明示的に書き込んだ形です。
The emergence of systems capable of contributing to mathematical research raises questions that cannot be answered by a technology company alone. There are many views as to the role of AI in mathematics, and we have deep respect and understanding for those concerned with its impact, including the signers of the Leiden declaration on AI and Mathematics ／ We hope the mathematical community will engage deeply with these results, place them in context, and bring the ideas behind them to life through new research and discovery. — 数学コミュニティへの姿勢に関する記述より
まとめ：「機械検証つき」をどう読むか
OpenAI Astra による今回の公表は、要点が3つあります。未解決問題10件という規模、Lean の証明ファイルという検証可能な形での公開、そしてAIの寄与を偽らないという著者性の表明です。とくに2つ目は、これまでの「AIが○○を解いた」という発表とは性質が違います。主張の当否を、第三者が自分の手元で機械にかけて確かめられます。
ただし「機械検証つき」という言葉を万能の保証と読むのは早いでしょう。検証の保証は、検証器の実装の質に乗っています。Astra の公表と同じ週に、Lean のカーネル自身の健全性バグが報告・修正され、それを突いた無効な「証明」が一度は受理されていた事実が明らかになりました。だからこそ、独立実装の検証器で突き合わせる導線が同梱されている点に意味があります。
A soundness bug in the Lean kernel ( #14576 ) was reported and fixed during the week of July 27. ／ On July 25, Ramana Kumar published a repository containing a sorry -free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. — 同じ週に Lean カーネルの健全性バグが報告・修正され、それを突いた無効な「証明」が存在した点の根拠として
実務的な読み方はこうなります。この成果は、数字ではなく手順で信頼を組み立てている。取ってきて、自分の環境で走らせ、別実装の検証器にもかける。そこまでやって初めて「確かめた」と言えます。AIが数学に踏み込む流れ自体はFable 5 のヤコビアン予想への挑戦からも続いており、当面は成果の主張よりも検証の作法のほうが論点になりそうです。
