AIが数学の未解決問題を10問解決｜OpenAI「Astra」の証明はどこまで確かめられたのか

2026年8月6日

OpenAIが8月1日、未公開モデルが解いた数学10問を証明つきで公開した

OpenAIが2026年8月1日、数学と理論計算機科学の未解決問題10件の解答を公式サイトで公開しました。解いたのは「Astra」というモデルです。OpenAIはAstraを次の主力モデルと位置づけていますが、まだ一般へ提供しておらず、今回使ったのはその社内版だと説明しています。

つまり、読者がいまChatGPTを開いて同じことを試せるわけではありません。Astraの提供時期も価格も、この発表では示されていません。

この種のニュースは、これまで確かめようがないものがほとんどでした。「AIが難問を解いた」と言われても、外部の人間が手元でできることが何もなかったからです。今回は事情が違います。OpenAIは249ページの論文に加えて、証明を機械が検算できる形に書き直したファイル一式をGitHubで公開しました。誰でもダウンロードして中身を見られます。

この記事では、OpenAIが実際に何を公開したのか、「機械が検証した」という言葉がどこまでを保証するのか、そして公開ファイルを実際に手元で確認した結果を順に見ていきます。数式には踏み込みません。

3分で把握

証明は機械が検算できる形で公開済み。数学者による検討は始まったばかり

2026年8月6日時点で確認できる範囲をまとめています。

解かれた問題

10件

どれも10年以上、主要な部分に進展がなかった問題です。

計算にかかった費用

2000ドル未満

10件を合わせた金額です。1問あたりではありません。

検算の状況

機械検証は完了

OpenAIの発表による。公開ファイルに未証明の穴がないことは本記事でも確認しました。

まだ済んでいないこと

査読の完了

専門家の検討は始まりました。失敗した試行の件数は未公表です。

解かれた10問は、どれも10年以上ほとんど動きがなかった

OpenAIは今回の10問について、「少なくとも10年、多くの場合はそれよりずっと長く、主要な結果に進展がなかった」問題を選んだと説明しています。分野は高次元の幾何から、通信の誤り訂正、群論、量子計算、格子暗号までかなり広く分かれています。一覧は下の表にまとめました。

1つだけ、日常の言葉で説明できる例を挙げます。「球の詰め込み」は、同じ大きさのボールを空間にどれだけ密に詰められるかを問う問題です。3次元なら、みかんを箱に詰めるときの話になります。ところが次元が4、5、100と増えていくと、最も密な詰め方がどれくらいの密度になるのか、誰にも分かっていません。今回Astraが出したのは、その密度の上限の見積もりを1978年以来はじめて改善する結果でした。

表に出てくる「Erdős問題」は、20世紀の数学者ポール・エルデシュ（Erdős Pál）が残した未解決問題の集まりです。1問ずつ番号が振られ、公開のデータベースで管理されています。今回はそのうち3件が解かれました。

「約2000ドル」は10問の合計であって、1問あたりではない

この発表で最も広まった数字が「約2000ドル」です。ただ、この金額が何を指すのかは、報道によって食い違っています。1問あたり2000ドルと書いている媒体もあります。

OpenAIの原文はこう書いています。

The total number of tokens needed to find solutions to these problems would cost roughly $2,000 at Sol API rates.

（これらの問題の解答を見つけるのに必要だったトークンの総量は、Sol APIの価格で換算すると約2000ドルになる）

「total（総量）」であり、10件を合わせた金額です。OpenAIの研究者Noam Brown氏も、Xへの投稿で「10件すべての証明生成にかかった費用は合計で2000ドル未満」と明言しています。1件あたりに直すと平均200ドル程度です。

引用にある「Sol API」は、すでに提供されている別のモデルの料金です。Astraは提供されていないため自身の料金表がなく、OpenAIはこの既存モデルの価格に当てはめて換算しています。

2000ドルに含まれているのは、AIが文章を生成するためのトークン代だけです。人間が結果を論文の形へ整えた作業は入っていません。後で見るように、失敗した試行の費用も入っていません。OpenAIがリポジトリに置いた設定ファイルには、この作業にかかった実時間が「約1週間」と記録されています。

機械による検算（Lean）が保証するのは、書かれた通りの論理に穴がないことだけ

今回の発表で、外部の人間が中身を確かめられるかどうかを分けたのは、証明をLeanという言語で書き直して公開した点です。

Leanは、数学の証明をプログラムが1行ずつ検算できる形に書くための言語です。人間が読む論文だと「ここは明らかなので省略する」と書ける部分も、Leanでは省略できません。すべての推論の段階を明示的に書き、それをLeanの検証プログラムに通します。通れば、書かれた論理に飛躍や穴がないことが機械的に確かめられます。

これは大きな前進です。従来なら「AIが証明したと言っている」で終わっていた話を、外部の人間が自分で検算できる形になりました。一方で、Leanが確かめてくれる範囲には、はっきりした境界があります。

「Leanが保証しないこと」として挙げた3点が、今回いちばん議論になっています。Leanは「書かれた文が証明されているか」を確かめますが、「書かれた文が正しい問題設定か」は確かめません。問題設定が正しいかどうかを判断できるのは、その分野を長く研究してきた人だけです。

実際、今回の結果の一部と近い領域で研究してきたコロンビア大学のHenry Yuen氏は、驚きを認めつつ、証明の書き方については批判しています。前置きの手続きを長く説明する一方で、技術的に肝心な部分をさらりと通り過ぎているため、何が新しいのかを読み取りにくいという指摘です（数学者の反応をまとめたOfficeChaiの記事より）。

公開されたLeanファイルを手元で確認した

「未証明の穴がない」という部分は、Leanの検証プログラムを走らせなくても、公開ファイルを読むだけで確かめられます。実際に手元で確認しました。

環境はmacOS（Darwin 25.5.0）で、2026年8月4日に openai/ten-proofs をコミット 94bc0fe の時点で取得しました。使ったのは git と grep と wc だけです。

手元で数えた結果

Leanのコード量

548,215行

10ファイルの合計

未証明のまま残した箇所

0件

sorry の記述なし

独自に追加した前提

0件

axiom 宣言なし

Leanの検算を通さない書き方

0件

native_decide 等なし

2026年8月4日、macOS上でコミット 94bc0fe を対象に確認。これはファイルの中身を読んだ結果であり、Leanの検証プログラムを実行した結果ではありません。

用語を3つだけ補足します。Leanでは、証明の途中を埋めずに先へ進めたいとき sorry と書きます。ここが残っていると、その証明には穴があります。axiom は、証明せずに前提として認めるルールを新しく足す書き方です。都合のよい前提を足せば何でも証明できてしまうため、追加されていないかどうかが重要になります。native_decide は、Leanの検証プログラムを通さずに計算結果を信用させる書き方です。

この3つがいずれも0件でした。OpenAI自身も設定ファイルで同じ内容を宣言していますが、その宣言と実ファイルが一致していることを外部から確かめられた、ということになります。使われている前提は propext、Classical.choice、Quot.sound の3つだけで、これらはLeanと標準ライブラリが普段から使っている土台です。

一方で、Leanの検証プログラムそのものは実行していません。実行するにはLean 4.32.0と数GB規模の標準ライブラリを新たに用意する必要があり、548,215行のビルドも長時間になります。ここでは「ファイルを読んで確かめた」以上のことは主張できません。証明が正しいことの根拠としては、OpenAIの公開物とその後の専門家の検証を待つ必要があります。

解けなかった問題が何問あったかは公表されていない

ここまでは公開されている情報の話でした。公開されていない情報もあります。

Noam Brown氏は別の投稿で、他の主要な問題にも挑戦して失敗したこと、ミレニアム懸賞問題はまだ解けていないことを認めています。ただし、何問に挑戦して10問が成功したのか、1問あたり何回試したのかは示されていません。

AI研究への批判で知られるGary Marcus氏は、自身のニュースレターでこの点を「分子だけがあって分母がない」と評しています。10という数字は出ているのに、その母数が分からないという指摘です。

失敗の件数が分からないと、2000ドルという数字の意味も変わります。「2000ドルあれば未解決問題が解ける」と受け取ると実態を外します。正確には、成功した10件のトークン代が合計2000ドル未満だった、という話です。失敗した試行を含めた総額はまだ公表されていません。

Anthropicの研究者は「同じ10問の半分は公開済みモデルで解けた」と投稿した

発表の翌日、別の角度から反応がありました。Anthropicに所属する数学者のLevent Alpöge氏が、同じ10問のうち5問を、すでに一般提供されているClaude Fableで24時間以内に解いたとXへ投稿しました。算術回路の計算量、量子ゲームの並列反復、最近ベクトル問題が含まれると説明されています。

Alpöge氏は設定も書いています。汎用的なプロンプトを与えただけで、モデルは完全に自律して動き、インターネットには接続していなかったとしています。同氏は7月20日にも、Claude Fable 5を使って87年間未解決だったヤコビアン予想の反例を示したと発表しており、この分野で続けて結果を出している人物です。

ただしこの投稿は、現時点では本人の申告にとどまります。OpenAIのようにLeanの証明ファイルは公開されておらず、第三者による検証も行われていません。Alpöge氏はAnthropicに所属していて、比較相手にあたる自社モデルの成績を報告している点も踏まえて読む必要があります。

それでも、この投稿が示した論点は残ります。今回の成果が未公開モデル固有の能力によるものなのか、それとも「機械検証と相性のよい問題を選び出した」ことの効果が大きいのか、まだ切り分けられていません。

AIによる数学の結果が続いた3か月

2026年5月

Erdősの単位距離予想の反証

OpenAIが未公開モデルの評価中に見つけたとして公表。後続の研究が5本続いた。

7月20日

ヤコビアン予想の反例

Levent Alpöge氏がClaude Fable 5を使い、87年間未解決だった予想の反例を示したと発表。

8月1日

Astraによる10件の結果

OpenAIが論文249ページとLean証明を同時公開。

8月2日

「半分は公開済みモデルで解けた」

Alpöge氏が、10問中5問をClaude Fableで24時間以内に解いたと投稿。

8月3日

外部の数学者による後続論文が2本

Fournier-Facio氏が非ソフィック群の後続論文を、Zhou氏がConnesの剛性予想の独立した反例をarXivへ投稿。

5月の件はOpenAIの発表内の記述、7月の件はFortuneの報道にもとづきます。

【8月6日追記】発表から2日で、外部の数学者が後続の論文を出した

公開から数日で、この記事の前提が1つ動きました。専門家の検討が「これから」ではなく、すでに始まっています。

最も具体的な動きは、ケンブリッジ大学の群論研究者Francesco Fournier-Facio氏が8月3日にarXivへ投稿した4ページの論文です。対象はAstraの10問のうち1問目、非ソフィック群です。これは「有限個の要素でできた構造をどれだけ持ってきても、決して近似しきれない群」のことで、そんな群が存在するのかが1999年から問われてきました。

Fournier-Facio氏は、Astraの証明の中核にある判定条件を取り出し、それを使ってOpenAIの方法では作れないタイプの例を新たに構成しました。同氏はこの判定条件をOpenAIの論文の「主要な新しさ」と書いています。

他人の証明の要点を理解し、それを使って自分の新しい結果を出す。これは、その論法を自分の研究で使えると判断した、という意味を持ちます。第三者が2日でそこまで進んだこと自体が、現時点で最も強い外部からの手応えです。

もう1つ、OpenAIの論文自体に書かれていて見落とされやすい記述があります。10問のうち4問目のConnesの剛性予想について、OpenAIは「原稿の準備中に、Shuoxing Zhou氏による独立かつ同時期の研究を知った」と明記しています。Zhou氏の論文も8月3日にarXivへ投稿され、GPT-5.6 Solの助けを借りて同じ結論に到達したと書かれています。つまり二組の研究が、別々の経路から同じ予想の反例へたどり着きました。

加えて、OpenAIの論文の謝辞を読むと、公開前に原稿を読んだ研究者の名前が章ごとに挙がっています。非ソフィック群の章ではHenry Bradford、Michael Chapman、Alon Dogon、そして前述のFournier-Facioの4氏。Connesの剛性予想の章では、OpenAIが今回あわせて答えたとする問いを提起した本人であるSorin Popa氏らです。まったく誰の目にも触れずに公開されたわけではありません。

2026年8月6日時点で確認できる外部の動き

後続論文が出た

非ソフィック群（1問目）

Fournier-Facio氏がAstraの判定条件を使い、別タイプの例を新たに構成。

独立に同じ結論

Connesの剛性予想（4問目）

Zhou氏が別経路で同じ反例に到達。こちらもAIの助けを借りています。

まだ動きが見えない

残り8問

公開された専門家の検証も、査読誌への採録もまだ確認できません。

arXivは投稿された論文を誰でも読める場所ですが、査読を経た掲載とは別のものです。ここに挙げた2本もまだ査読前です。

ここまでを踏まえても、記事の結論は変わりません。動きがあったのは10問のうち2問で、どちらも査読を通ったわけではありません。ただ、「誰も中身を見ていない」という段階は過ぎました。

それでも、この発表が従来と違うのは証明を全部公開した点にある

ここまで未確認の部分を並べてきたので、逆側も書いておきます。

まず、証明が公開されている点そのものが従来と違います。企業がAIの成果を発表するとき、外部が確かめられる材料まで出す例はほとんどありませんでした。今回は論文、Leanの証明、思考過程の記録、独立検証用の設定までがApache-2.0ライセンスで公開されています。反論したい研究者は、実際に手を動かして反論できます。

次に、公開されたLeanファイルには前述のとおり未証明の穴がありません。都合のよい前提を足したり、検算を迂回したりした形跡もありませんでした。この規模の証明を548,215行まで書き切って穴を残さなかったこと自体、簡単な作業ではありません。

数学者の反応も否定一色ではありません。OfficeChaiが集めた反応によれば、トロント大学のDaniel Litt氏は今回の結果を大きな出来事だと評価しています。一方でスタンフォード大学のJared Duker Lichtman氏は、印象的ではあるが驚きはないと述べています。反応が分かれているのは結果の真偽ではなく、これを能力の飛躍と見るか、既存の延長と見るかという評価の部分です。

いま読者に関係するのは、AIの成果を自分で確かめる手段が増えたこと

この発表で、明日から生活や仕事が変わることはありません。Astraは提供されていませんし、解かれた10問はどれも純粋な理論の問題です。

1つだけ誤解されやすい項目があるので触れておきます。10問のうち7番目は、格子暗号の土台になっている「最近ベクトル問題」を扱っています。格子暗号は、将来の量子コンピュータでも破られにくい暗号として実用化が進んでいる方式です。ただし今回の結果は、この問題が従来考えられていたより難しいことを示す方向のものです。いま使われている暗号がすぐ破られる、という話ではありません。

読者にとって実際に変わるのは、成果の確かめ方だと思います。「AIがすごい結果を出した」という発表に対して、これまでは信じるか疑うかしか選べませんでした。証明や検証手順まで公開されると、第三者が中身を見て是非を言えます。今回のように、報道の数字（1問2000ドル）と原文（合計2000ドル）のずれも、原文を開けば数分で分かります。

OpenAI自身も、数学界からの批判を意識した書き方をしています。発表文では、AIが生成した証明に人間の著者名を付けることは実態を偽ることになる、と明記しました。2026年6月に15大学の研究者16名が公表し、国際数学連合が支持を表明したLeiden宣言にも言及しています。この宣言は、AIが生成した証明の信頼性、成果を誰の功績とするか、査読の維持について提言をまとめたものです。

まとめ: いまは「査読前の10件の結果」として受け取るのが実態に近い

現時点で言えることを整理すると、次のようになります。証明は機械が検算できる形で公開され、未証明の穴はありません。専門家による検討は10問のうち2問で動き始めましたが、査読を通った結果はまだ1件もありません。失敗した試行の件数は公表されておらず、Astra自体も使えません。

今後、確度を上げてくれる材料は3つあると考えています。残りの問題についても専門家が定理文を精査した結果、失敗率を含めた開示、そしてAstraが提供されて第三者が同じことを再現できるようになるかどうかです。1つ目は8月3日の2本で動き出しました。全体像が見えるまでには、まだ数か月かかるとみています。

もし今後、同じような「AIが難問を解いた」というニュースを見かけたら、証明が公開されているか、機械で検算できる形になっているか、失敗した試行の数が書かれているかの3点を見てください。今回の発表は、最初の2つを満たして3つ目を欠いている、という位置にあります。