「みなづちAI」はリンクフリーです。リンクを行う場合の許可や連絡は不要です。引用する際は、引用元の明記と該当ページへのリンクをお願いします。
OpenAIの数学10件。原文のadvancesが日本語では「解決」になった
みなづちです。
2026年8月3日の朝、日本語のニュースサイトに同じ話題が並びました。OpenAIの次期主力モデル「Astra」が、数学の未解決問題10件で成果を出した、という内容です。
ITmediaは午前6時56分、Impress Watchは午前8時に記事を出しました。どちらも8月1日に公開されたOpenAIの発表を伝えるものです。
Astraという名前が公になったのは、これが初めてです。いま使えるGPT-5.6の次に来る主力モデルにあたります。
命名も揃っています。GPT-5.6のSol（太陽）、Terra（地球）、Luna（月）に続く天体の名前で、Astraはラテン語で「星々」を意味します。
ただ、OpenAIの原文と日本語の見出しを並べると、使われている語の強さが違っていました。本記事では、そこから話を始めます。
本記事では、以下のポイントから解説します。
- OpenAIが公表した10件の中身と、原文が実際に使っている語
- 249ページの原稿とGitHubで公開されたLean証明の中身
- 発表の4日前に、AI支援で作られた証明がLeanのバグを突いていた経緯
- Astraへの直接の反応と、それ以前からある懸念の区別
- Astraはいつ使えるのか。日本の料金表で今日触れるモデルはどれか
目次
結論：公式タイトルは「10の前進」。日本語では「解決」に変わった
まず記事全体の結論からお伝えします。今回の発表で押さえておきたいのは、OpenAIの公式タイトルが「解決」ではなく「前進」だったという点です。
公式ページのタイトルは「Ten advances in mathematics and theoretical computer science」です。advances、つまり前進です。
一方、日本語の見出しはこうでした。ITmediaは「未解決の数学問題10件を「解決」と発表」。Impress Watchは「数学の未解決問題を解決」です。
ここで正確を期しておきます。OpenAIが控えめな語だけを使っているわけではありません。本文にはdisprovesやresolving、provedといった語も出てきます。10件のうちいくつかは、はっきりと反証や解決として書かれています。
避けられているのは solve という語だけで、ページ本文に0件でした。ただし249ページの原稿の側では solve が使われています。
つまり変わったのはタイトルの語です。advances（前進）という枠づけが、日本語では「解決」の2文字に置き換わりました。ITmediaは「解決」にカギカッコを付けて留保しましたが、Impressは地の文で断定しています。
数字も成果も本物です。10件の内容も、Lean 4での形式化も、GitHubでの公開も、実際に確認できます。ただし外部の数学者による査読は現時点で未了です。ここを押さえて読むのが今回の要点です。
筆者の視点：3つの見出しを並べたら、語の強さが変わっていった
この発表を追う中で、読み方が途中で変わった経験があります。ここではその過程を書きます。
同じ発表なのに、経路を通るたびに強くなっていた
最初に見たのはITmediaの見出しでした。「解決」にカギカッコが付き、さらに「と発表」が添えられています。断定を二重に避けた形です。
その約1時間後に出たImpress Watchの見出しには、カギカッコも「と発表」もありませんでした。地の文で「解決」と書いています。
そして原文にあたると、タイトルはadvancesでした。3つを並べると、前進→「解決」と発表→解決、という順に主張が強くなっていきます。
誰かが嘘をついたわけではありません。要約のたびに限定語が落ちただけです。ただ、受け取る側に届くのは最後の形だという点は、意識しておく必要があると感じました。
249ページの原稿を開いたら、Astraの語がなかった
もうひとつ気になったのは、Astraという名前がどこに書かれているのかでした。
公式ブログには「The results were achieved by an internal version of Astra, our next major model」とあります。次期主力モデルAstraの社内版による成果だ、という書き方です。
ところが、根拠として公開されている249ページの原稿を全文検索すると、Astraという語は一度も出てきません。要旨の主語は「an internal OpenAI model」で統一されています。
PDFのメタデータの件名も「A collection of research papers by an internal model at OpenAI」です。著者名も個人名ではなく「OpenAI」でした。
これは矛盾ではありません。ただ、モデル名を前面に出したのは広報の側で、学術的な成果物の側は匿名のままだという構造は、記録しておく価値があると考えています。
8月1日に公表された10件と、約2,000ドルという数字の条件
ここで押さえておきたいのは、何がどの分野で主張されているのかという点です。原稿の要旨と突き合わせると輪郭がはっきりします。
高次元球充填から極値グラフ理論まで、8分野の10件
公式が挙げる分野は、高次元幾何、符号理論、算術回路計算量、群論、作用素環論、量子計算量、格子暗号、極値組合せ論の8つです。
そこに10件の結果が並びます。目立つものから見ていきます。まず高次元の球充填があります。空間にできるだけ密に球を詰める問題で、その一般的な上界を表す指数が改善されました。
原稿にはこう書かれています。「This is the first improvement since 1978 to the general sphere-packing exponent」。1978年以来、一般の球充填指数が改善されるのは初めてだという主張です。
ここで注意が必要です。改善されたのは詰め込みの密度そのものではなく、理論的な上界を表す指数です。従来の値0.59905576…に対し、新しい値は0.6044…とされています。
非ソフィック群、コンヌの剛性、エルハートの体積予想
ほかに並ぶものにも、一言ずつ添えておきます。
非ソフィック群は、可算無限の群のかけ算表の有限部分を、有限集合の上の置換でどこまで正確に真似できるか、という問いに関わります。真似できない群が存在するかは長く問われてきました。今回その例が構成されたとされています。
コンヌの剛性予想は、群を作用素環という「影」に落としたとき、影から元の群を復元できるかという問いです。
ただし予想は、ICC（自明でない共役類がすべて無限）かつ性質(T)という強い条件を満たす群に限った話です。条件を外せば復元できないことは1976年から知られています。今回はその限定つきでも復元できない例が示された、という主張になります。
エルハートの体積予想は、重心が内部で唯一の格子点になっている凸な立体の体積は、単体が最大か、という問題です。上界は(n+1)^n/n!とされました。ただし最大を与えるのが単体だけかどうかは、原稿自身が未解決だと書いています。
約2,000ドルは実費ではなく、別モデルの料金に換算した値
一般の関心を最も引いたのが費用の数字でした。10件の結果を得るのに約2,000ドル、日本円で約32万円という数字です。
ただし原文には条件が付いています。「The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates」。
would cost、つまり仮定法です。実際に支払った額ではなく、消費したトークン量をGPT-5.6 SolのAPI料金に換算したらいくらになるかという試算です。
条件はほかにもあります。10件の合計であって1件あたりではないこと、換算に使ったのはAstraではなく別モデルSolの料金であること、トークン数の実数は非開示であること、そして「roughly」と概算であることです。
さらに、この2,000ドルは成功した10件の分だけです。何件試して10件に至ったのかという分母は公表されていません。
249ページの原稿に「Astra」の語は一度も出てこない
この点について端的に言えば、公開されている成果物と広報上のモデル名が、別のレイヤーに置かれているということです。
帰属の方針は三重に書かれている
OpenAIは成果の帰属について、踏み込んだ書き方をしています。
AIが完全に生成した証明を人間の著作として主張することは、システムの貢献と人間の知的作業の本質の両方を誤って表す、という趣旨です。
原文の要になる部分は「would misrepresent both the system’s contribution and the nature of genuine human intellectual work」です。
形式化を誰がやったのか、記述が揺れている
ただし、工程の説明には気になる箇所があります。誰が何をやったのかが、3通りに書かれているのです。
1つ目は「These arguments were then prepared into manuscripts by humans with the same model」。人間が同じモデルを使って原稿にした、という書き方です。
2つ目は「Afterward, the model formalized each argument in a Lean certificate」。モデルが各議論をLean証明に形式化した、となります。
3つ目は「We helped prepare the manuscripts and formalize the proofs in Lean, and we take responsibility for their correctness」です。
我々が原稿化と形式化を手伝い、正しさの責任を負う、という書き方になっています。
モデルがやったのか人間が手伝ったのか、同じページの中で表現が揺れています。成果の帰属を明確にすると宣言している文書だからこそ、ここは押さえておくべきだと考えています。
Lean 4で形式化しGitHubへ公開。未証明の穴は0件だった
ここでのポイントは、今回の発表が従来の「AIが数学の問題を解いた」という主張と何が違うのかという点です。差は形式化にあります。
Leanとは証明支援系と呼ばれるソフトウェアです。数学の証明を、人間が読む文章ではなくコンピュータが検査できる形式で書き、論理の飛躍がないかを機械的に確かめられます。
GitHubのopenai/ten-proofsに何が置かれているか
公開されたリポジトリはApache 2.0ライセンスで、言語はLeanです。10件の advances に対応するファイルが並んでいます。
サイズも確認できます。最大は最近ベクトル問題のファイルで約5.34MB、次いで符号のファイルが約4.53MBです。人間が通読できる分量ではありません。
なお、コミット履歴は実質1件だけです。コミットメッセージは半角ピリオド1文字で、開発の経過を残さずまとめて投下された形になっています。
sorryが0件で、使われている公理は標準の3つだけ
形式化の品質を示す情報も、設定ファイルに書かれています。
Leanには「sorry」という仕組みがあります。証明の途中を埋めずに飛ばすための記述で、これが残っていると証明は完成していません。
公開された設定ファイルにはsorry_countが0、定義中のsorryも0と記されています。未証明の穴は残っていない、という主張です。
使われている公理も列挙されています。propext、Classical.choice、Quot.soundの3つで、Leanで通常使われる標準的な組み合わせです。特殊な仮定を持ち込んではいません。
10件の advances に対して、形式的な結果は12件が登録されています。2つのファイルがそれぞれ2つの結果を含むためです。
レビューの状態は「エージェントによるレビュー」だった
一方で、同じ設定ファイルには見落とされがちな記述もあります。レビューの状態を示す項目です。
そこには「agent-reviewed」と書かれています。人間の査読ではなく、エージェントによるレビューを経た、という意味です。
書いたのがAI、レビューしたのもAI、検証するのが機械という構成になります。分量を考えれば人間が全行を読むのは現実的ではないため、これ自体は自然な設計とも言えます。
ただし「形式検証済み」という言葉から、外部の第三者が確認したという印象を受けるとすれば、それは正確ではありません。8月3日時点で、独立した検証の報告は確認できていません。
発表の4日前、AI支援の証明がLeanのバグを突いていた
この問題の核心は、機械検証という土台そのものが、直前に揺れていたという事実にあります。しかも揺らしたのは、AIが関わった証明でした。
コラッツ予想の「反証」から見つかった
2026年7月25日、ラマナ・クマール氏がコラッツ予想の反証を主張するリポジトリを公開しました。300行に満たない短いLean証明で、AI支援で作られたものとされています。
コラッツ予想は、どんな正の整数から始めても決まった操作を繰り返せば必ず1に到達する、という有名な未解決問題です。それが300行で反証されたなら、大変な出来事になります。
7月28日、キラン・ゴピナサン氏がこれをレビューする中で異常に気づき、Leanのリポジトリに課題を立てました。番号は14576です。
タイトルは「Kernel accepts wrong-structure projections, allowing an axiom-free proof of False」。カーネルが誤った構造の射影を受理し、公理を使わずに「偽」を証明できてしまうという内容でした。
証明が正しかったのではなく、証明を検査する側に穴があった、ということです。
修正は同日、リリースは同日、公式見解も出た
対応は速いものでした。修正はLeanの開発を率いるレオナルド・デ・モウラ氏によるもので、報告から数時間でマージされています。修正版のLean 4.32.2も同日中に公開されました。
デ・モウラ氏はポストモーテムも公開しています。そこで示された見解は、これは実装のバグであってLeanのメタ理論の穴ではないというものです。
バグに到達するにはメタプログラム経由で宣言をカーネルへ直接送る必要があり、通常の証明では引数が型検査されて弾かれる、とも説明されています。
さらに厄介な点も明かされました。外部チェッカであるnanodaにも別のバグがあり、クマール氏は両方を同時に突く証明項を書けることを実演していたのです。二重チェックが同時に破られたことになります。
公式リリースノートには、この一文があります。「The bug can be exploited even when using comparator」。照合用の仕組みを使っていても悪用できた、という意味です。
公開リポジトリは修正前のv4.32.0を使っていた
ここで確認しておきたいのが、OpenAIが公開したリポジトリの使っているLeanのバージョンです。
lean-toolchainというファイルに書かれていたのは「leanprover/lean4:v4.32.0」でした。健全性バグが修正されたv4.32.2より前のバージョンです。
リポジトリには8月2日にもpushがありますが、toolchainは更新されていません。修正版で再検証したかどうかについて、OpenAI側の言及は確認できていません。
念のため付け加えると、公開されたファイルにバグへ到達するようなメタプログラムは見当たりませんでした。危険があると言いたいわけではありません。
ただ、Lean公式のリファレンスには、脅威モデルの説明として次の一文があります。「This includes un-reviewed AI-generated proofs and programs」。レビューを経ていないAI生成の証明は、敵対的な入力として扱えという位置づけです。
コラッツの件は、まさにその実例でした。そしてその4日後に、同じカーネルで検証されたAI生成の証明が10件公開されたことになります。
Erdős問題のデータベースは、まだ解決扱いにしていない
ここでのポイントは、数学界の側の受理プロセスがどう動いているかという点です。無反応ではありませんが、解決扱いにもなっていません。
3件とも「OPEN (LEAN)」というラベルに変わっていた
OpenAIの公式ブログとGitHubのREADMEは、Erdős問題の番号を挙げています。多色ラムゼー数で183番、極値グラフ理論で146番と180番を resolving するものだという書き方です。
Erdős問題には公式のデータベースがあります。erdosproblems.comというサイトで、マンチェスター大学のトーマス・ブルーム氏が運営しています。
2026年8月3日に確認したところ、3件とも解決扱いにはなっておらず、ステータスは「OPEN」のままでした。
ただし無反応ではありません。8月1日以降、3件のラベルが「OPEN (LEAN)」という表記に変わっています。他のOPEN問題には見られない書き方で、8月1日付のコメントも付いていました。
なお公式ブログは180番と書いていますが、249ページの原稿はコンパクト性予想の出典として575番を引用しています。番号の対応がずれている可能性があり、ここは断定を避けるべき箇所です。
5月の成果は同日に反映され、Leanタグは約1か月後だった
比較になる事例があります。OpenAIは2026年5月にも、未公開モデルでErdősの単位距離問題を反証したと発表しています。
同じデータベースでその問題を確認すると、現在の状態は「DISPROVED (LEAN)」です。備考には「OpenAIの社内モデルによって反証された」と明記されています。
過去の記録をたどると、動きは2段階でした。ステータスが「DISPROVED」に変わったのは発表と同日の5月20日です。
そして「(LEAN)」というタグが付いたのは、それから約1か月後でした。ステータスの更新と、Lean検証の確認は別のタイミングで行われていることになります。
今回の3件も、同じ経路をたどる可能性はあります。8月3日時点では、その途中だと見るのが正確です。
Astraへの反応は2件。ガワーズ氏の言葉はAstraへの評価ではない
この点の結論を先に言えば、英語圏で語られていることを一括りにすると、対象を取り違えるということです。
Astraへの直接の反応は、限られている
8月3日時点で、Astraの発表そのものへの反応として確認できたのは2件です。
ひとつはトーマス・ブルーム氏の評価です。同氏はXで「big news」と述べたと報じられています。ただし言葉には留保が付いていました。
「Maybe not bigger than a proof of unit distance would have been, but in terms of constructions, this is big」。
単位距離予想の証明が仮に出ていたとしたら、それより大きくはないかもしれない。ただ構成という点ではこれは大きい、という趣旨です。
比較の相手は5月に実際に出た反例ではなく、仮定の話です。ここを取り違えると、評価の強さが変わってしまいます。同氏はAIが数学者を置き換えるという見方も否定しています。
もうひとつはゲイリー・マーカス氏の論考です。2026年8月2日に「OpenAI’s amazing — but vastly oversold — new model Astra」を公開しました。驚異的だが大幅に過大宣伝されている、という立場で、7つの留保を挙げています。
主な論点は、手法の詳細が示されておらず科学というよりマーケティングに近いこと、一部の数学に強いことと「数学が解決した」ことは違うこと、などです。
ガワーズ氏とタオ氏の言葉は、Astraへの反応ではない
ここで区別が必要になります。英語圏の記事で引かれているフィールズ賞受賞者の言葉が、Astraへの反応として紹介されることがあるからです。
ティモシー・ガワーズ氏の「possible destruction of mathematical culture」という言葉は、確かに強い表現です。ただし出典はライデン宣言に関する同氏自身のブログ投稿で、Astraの発表より前の文脈です。
「足元の絨毯を引き抜かれるような感覚だった」という発言も同氏のものですが、こちらはGPT-5.6 Proが同氏の取り組んでいた問題を初回で解いたことについてでした。
テレンス・タオ氏の懸念も同様です。証明が生成される速度に人間の検証が追いつかなくなるという「proof overload」の指摘は、2026年の国際数学者会議での講演が出典です。
いずれもAI全般に対する懸念であって、Astraを名指しした評価ではありません。同じ記事に並んでいても、対象は別のものだということになります。
成果の限界も、同じ記事に書かれていた
もうひとつ、日本語では見かけなかった記述にも触れておきます。
Astraの技術に関わるOpenAIの研究者であるノーム・ブラウン氏は、発表に際してこう投稿したと報じられています。「Sadly, no Millennium Prize Problems (yet)」。
ミレニアム懸賞問題という、数学で最も難しいとされる7つの問題には手が届いていない、という趣旨です。成果を出した側が自ら限界を示していたことになります。
日本語2紙が書かなかったのは、査読と第三者による検証だった
この話が日本の読者にどう関わるのかを整理します。結論から言えば、日本語だけを読んでいると賛否の存在が見えません。
両紙の本文を確認したが、査読と第三者検証の記述はなかった
ITmediaとImpress Watchの本文を、それぞれ逐語で確認しました。
まず正確を期しておきます。ITmediaは検証の話に触れていないわけではありません。Leanによる形式証明、GitHubでの公開、OpenAIが正しさの責任を負う旨を、いずれも本文に書いています。
書かれていないのは、外部の数学者による査読と、第三者による独立検証です。マーカス氏の留保も、ブルーム氏の評価も、データベースがまだOPENであることも、記事には含まれていません。
Impress Watchの本文は、さらに情報量が少なくなります。Lean、形式証明、GitHubへの言及がいずれも0回でした。両紙を同質のものとして扱うのは正確ではありません。
ITmediaの本文は、見出しより慎重に書かれている
公平を期して、ITmediaの本文の書きぶりにも触れておきます。
「新たな結果を得たと発表した」「Astraの社内版によるものだとしており」「〜としている」といった書き方で、記者による事実断定がありません。伝聞の形が徹底されています。
さらにITmediaは、読者が最も知りたい部分について正確に書いています。「Astraの公開時期やモデル構成、API料金、ChatGPTでの提供形態などは明らかにしていない」という一文です。
書かれていないことを、書かれていないと明示する。これは記事として誠実な処理だと感じました。
見出しだけが独り歩きし、限定語が消えていく
問題は、多くの読者が本文まで読まないことです。ソーシャルメディアで流れるのは見出しで、そこには「解決」の2文字が残ります。
原文のタイトルがadvancesであること、データベースがまだOPENであること、Leanの土台に4日前まで穴があったこと、成果を出した側が「ミレニアム懸賞問題には届いていない」と述べていること。これらは見出しからは見えません。
情報を要約する過程では、必ず何かが削られます。削ってはいけないものが何かを見分けることが、受け取る側にも求められているのだと思います。
Astraは料金表のどこにもない。今日使えるのはGPT-5.6系
日本の読者にとっての実利をまとめます。結論から言えば、Astraは今日の時点では誰も使えません。
API価格表にもChatGPT料金表にもAstraはない
OpenAIのAPI価格表を確認しました。標準ティアの短いコンテキストで、100万トークンあたりGPT-5.6 Solが入力5ドルと出力30ドル、Terraが2ドルと12ドル、Lunaが0.20ドルと1.20ドルです。
条件が付く点は押さえておきます。長いコンテキストではSolが10ドルと45ドルになり、倍以上です。データレジデンシー対応のリージョンを使う場合は10%が上乗せされます。
ChatGPTの料金ページも確認しました。比較表に並ぶのはGPT-5.5 Instant、GPT-5.6 Sol、GPT-5.6 Sol Pro、GPT-5.6 Terra、GPT-5.6 Luna、GPT-5 Thinking Miniです。
どちらの表にもAstraは載っていません。公開時期も、価格も、ChatGPTへの搭載形態も、日本語で使えるかどうかも、すべて未発表です。
日本のChatGPT料金と、Plusで使えるモデル
日本のChatGPT料金は、無料版が0円、Goが月額1,400円、Plusが月額3,000円、Proが月額16,800円からです。
Plusで使える最上位の推論モデルはGPT-5.6 Solです。ただしPlusではTerraもLunaもGPT-5.5 Instantも使えます。Sol専用というわけではありません。
ひとつ注意点があります。Sol ProはProプラン向けとされていますが、これは英語版の料金ページの表記です。日本語版のページではPlusでもSol Proが「拡張」と表示されており、公式サイト内で記載が食い違っています。
いずれにしても、今日Plusに課金して使えるのはGPT-5.6系の既存モデルであって、Astraではありません。
Googleの「Project Astra」との名前の衝突に注意
もうひとつ、実務的な注意点があります。Astraという名前は、この件に固有のものではありません。
Googleが2024年5月に「Project Astra」を発表しており、日本語で「Astra」を検索すると、そちらの記事が上位に出てくることがあります。
なお、どちらも正式なモデル名ではありません。Google側は研究プロトタイプの名称で、OpenAI側も報道によれば仮称とされています。情報を追う際は発表元と日付を確認する必要があります。
AIが証明を書く速度に、人間が検証する速度が追いついていない
今回の発表を通して見えてくるのは、生成の速度と検証の速度が大きく離れたという事実です。開発期間は1週間、消費したトークンをSolの料金に換算すれば約2,000ドル。この速さは疑いようがありません。
同時に、受け取る側の状況もはっきりしました。公開された形式化は数MB規模のファイルが並び、人間が通読できる分量ではありません。レビューの状態は「エージェントによるレビュー」と記されています。
Erdős問題のデータベースは、5月の成果を発表と同日にステータス変更しましたが、Lean検証のタグを付けるまでには約1か月かかりました。今回の3件は、8月3日時点でその途中にあります。
そして機械検証という土台自体も、絶対ではないことが直前に示されました。7月25日にAI支援で作られたコラッツ予想の反証が公開され、7月28日にそれがLeanのカーネルバグを突いていたことが判明しています。
デ・モウラ氏はこれを実装のバグでありメタ理論の穴ではないとしたうえで、同日中に修正しました。対応は速く、透明でした。
ただし外部チェッカのnanodaにも別のバグがあり、両方を同時に突く証明項が書けることも実演されています。二重チェックの安全性は「全チェッカに同時に効くバグはない」という仮定の上にあります。
これらはOpenAIの成果を否定する材料ではありません。1978年以来動かなかった球充填指数が更新されたのなら、それは大きな出来事です。ブルーム氏が「big news」と評したのも、成果を本物と受け止めたからでしょう。
ただ、そのうえで確認しておくべきことがあります。公式タイトルはadvancesであり、データベースはまだ解決扱いにしていません。独立した検証の報告もありません。次に見るべきなのは、次の10件が出るかどうかではなく、この10件が数学界に受理されるかどうかだと考えています。
まとめ：OpenAIの数学10件をめぐる6つの要点
ここまでの内容を整理します。今回の発表は、成果の大きさより、その成果がどう表現され、どう受け取られたかを確認することが重要でした。
- 公式タイトルはadvances（前進）： 本文にdisprovesやresolvingは使われているが、タイトルの枠づけが日本語では「解決」に置き換わった
- 249ページの原稿にAstraの語は0件： 主語は「社内のOpenAIモデル」で統一。モデル名が出るのは広報側の文書だけ
- 約2,000ドルは実費ではない： 消費トークンをGPT-5.6 SolのAPI料金に換算した仮定計算値。試行総数という分母も非公開
- 4日前にAI支援の証明がLeanのバグを突いていた： 7月25日公開のコラッツ反証が発端で、7月28日に修正。公開リポジトリはその前のバージョンを使っている
- 数学界はまだ解決扱いにしていない： データベースは3件ともOPEN。ただしラベルが「OPEN (LEAN)」に変わっており、無反応ではない
- Astraは今日誰も使えない： API価格表にもChatGPT料金表にも記載なし。日本でPlusに課金して使えるのはGPT-5.6系まで
AIが数学の最前線に届き始めたこと自体は、疑いようのない出来事です。だからこそ、誰が何をどう言ったのかを正確に区別しておくことが、いま必要なことだと考えています。
よくある質問（FAQ）
Q1. Astraはいつから使えるようになりますか。
A. 現時点では未発表です。OpenAIが公式に書いているのは「次期主力モデルの社内版による成果」という位置づけまでで、公開時期、モデル構成、API料金、ChatGPTへの搭載形態のいずれも明らかにされていません。日本語対応についても記載がありません。ITmediaも記事の中で同趣旨を明記しています。API価格表にもChatGPTの料金比較表にもAstraの記載はなく、今日課金して使えるのはGPT-5.6系の既存モデルです。なお、Astraは報道によれば仮称とされており、正式名称が変わる可能性もあります。
Q2. 「Leanで検証済み」なら、証明が間違っている心配はないのですか。
A. 形式化そのものは実在し、未証明の穴を示すsorryは0件、使われている公理も標準的な3つだけだと公開情報に記されています。ただし2つ留保があります。ひとつは、発表の4日前にあたる2026年7月28日、Lean本体のカーネルに公理を使わず「偽」を証明できるバグが見つかり、同日に修正されたことです。きっかけはAI支援で作られたコラッツ予想の反証で、公式リリースノートには照合用の仕組みを使っていても悪用できたと明記されています。公開されたリポジトリが使っているのは、その修正が入る前のバージョンです。もうひとつは、レビューの状態が「エージェントによるレビュー」と記されており、人間の査読を経たものではない点です。
Q3. Erdősの未解決問題が3つ解決されたということですか。
A. OpenAIの公式ブログとGitHubのREADMEは、146番、180番、183番の3件について resolving（解決するもの）と書いています。ただし公式のデータベースであるerdosproblems.comを2026年8月3日に確認したところ、3件ともステータスは「OPEN」のままでした。無反応というわけではなく、8月1日以降にラベルが「OPEN (LEAN)」という他の問題には見られない表記へ変わっており、8月1日付のコメントも付いています。同じデータベースは5月の単位距離問題の反証については発表と同日にステータスを更新し、Lean検証のタグはさらに約1か月後に付けました。現時点では「解決されたと主張され、確認の途中にある」段階と理解するのが正確です。
筆者より
この記事は一度書き上げたあと、ファクトチェックで骨格から書き直しました。
最初に立てた軸は「OpenAIは解いたと書いていない」というものでした。solveという語が本文に0件だったからです。
ところが調べ直すと、disprovesもresolvingもprovedも使われていました。solveだけを見て「控えめだ」と結論づけたのは、早合点でした。
正確には、変わったのはタイトルの枠づけです。advances（前進）が日本語では「解決」になった。事実としてはこちらのほうが小さく見えますが、検証に耐えるのはこちらです。
もうひとつ、書き直しで大きく変わったのがコラッツ予想の件でした。当初は人間が書いた証明だと理解していたのですが、AI支援で作られたものでした。AIが関わった証明が検証系のバグを突き、その4日後に別のAI生成証明が同じ検証系で公開された。この時系列こそが、今回いちばん書くべきことだったと思っています。
参考資料
- OpenAI公式ページ「Ten advances in mathematics and theoretical computer science」（2026年8月1日）
- OpenAI「ten-proofs」249ページのPDF原稿（cdn.openai.com）
- GitHub openai/ten-proofs（README、lean-toolchain、formalization.yaml）
- Lean 4.32.2 公式リリースノート（2026年7月28日）
- レオナルド・デ・モウラ氏によるポストモーテム（2026年7月28日のカーネル健全性バグについて）
- leanprover/lean4 issue #14576 および修正PR #14577（2026年7月28日）
- Lean公式リファレンス「Validating a Lean Proof」（脅威モデルの記述）
- xrchz/CollatzLean リポジトリ（2026年7月25日公開）
- erdosproblems.com（トーマス・ブルーム氏運営）問題146・180・183・90の各ページ（2026年8月3日確認）
- ITmedia NEWS（2026年8月3日06時56分）
- Impress Watch（臼田勤哉氏、2026年8月3日08時00分）
- the-decoder「OpenAI announces its “next major model” Astra by dropping ten previously unsolved math solutions」（マティアス・バスティアン氏、2026年8月1日）
- the-decoder「AI keeps cracking unsolved math problems, and mathematicians have mixed feelings」（同氏、2026年8月1日）
- Gary Marcus「OpenAI’s amazing — but vastly oversold — new model Astra」（2026年8月2日）
- OpenAI API価格ページ（platform.openai.com/docs/pricing）
- ChatGPT料金ページ（openai.com/chatgpt/pricing、日本語版を含む、2026年8月3日確認）
- Google公式ブログ Google I/O 2024 発表一覧（2024年5月）
この記事が気に入ったら
フォローしてね！
お気軽にコメントどうぞ