OpenAI、次期モデル「Astra」で未解決の数学難問10件を攻略　証明はLeanで検証

AIは既存の知識をまとめるのは得意でも、未解決の難問を突破するような本物の数学的推論はまだ無理だろう。そう考えていた人にとって、今回の発表は強烈なカウンターになるはずです。

OpenAIは開発中の次期主力モデル「Astra」の内部バージョンを使い、数学および理論計算機科学における10件の未解決問題を解決、あるいは大きく前進させたと発表しました。いずれも少なくとも10年以上、中には約30年間にわたり誰も解けなかった難問です。

何より驚かされたのはその費用です。10問すべての解法探索に要したトークン量は、Sol APIの利用料に換算するとわずか約2000ドル相当でした。

半世紀級の予想反証からエルデシュ問題まで

攻略された10件は、高次元幾何学、符号理論、算術回路の計算量、群論、作用素環、量子計算量、格子暗号、極値組合せ論など多岐にわたります。

例えば群論では、1999年以来数学者が探し続けていた「非sofic群」の存在を具体的に構成して示しました。さらに、フォン・ノイマン環に関するアラン・コンヌの剛性予想を反証し、エルハルトの体積予想を高次元で決定。パウル・エルデシュが残した3つの未解決問題（146番、180番、183番）にも決着をつけました。

耐量子暗号の基礎となる格子暗号の「最近ベクトル問題（CVP）」でも近似の困難性を証明したほか、高次元球充填密度の理論上限値の更新など、学術的に極めて重い成果が並んでいます。

OpenAIによれば、数学的論証はすべてAstraが自律的に考案し、人間とモデルが共同で論文形式にまとめました。さらに、その証明は証明支援系「Lean」の証明書として形式化検証済みです。思考プロセスの推論ログも公開されています。

発表直後の業界の動きも機敏でした。わずか24時間後には、AnthropicのLevent Alpoge氏が自社のモデル「Fable」を使い、一般的なプロンプトとオフライン環境で10問中5問の証明を再現できたと主張しています。

論文の著者権とライデン宣言

AIが核心部分を考えたとき、著者は誰になるのか。OpenAIはこのセンシティブな問題にも踏み込み、「AIと数学に関するライデン宣言」に署名した数学者たちの懸念に敬意を表しています。

同社は、AIが完全に導き出した証明に人間の著者名を付けるのは、AIの貢献と人間の知的労働の双方を偽ることになると指摘。論証そのものはAstraが生成したとし、人間側はLeanでの検証と論文執筆の正確性に責任を持つという立場をとりました。すでに業界内では「この成果はフィールズ賞級なのか」という議論が巻き起こっています。

なぜ重要か

私たちが最も注目すべきだと考えるのは、やはり「2000ドル」という数字です。

これまで、フロンティアAIを使った高度な科学研究は莫大な計算資源を持つ巨大テックの独壇場と見られていました。しかし、10年間誰も手が出なかった難問を10個片付けるコストが数十万円程度で済むなら、一般の研究室や個人の数学者でも現実的に活用できるようになります。

また、Anthropicが翌日に5件を再現した事実が示すように、最先端モデルの間で論理推論の能力差は急速に縮まっています。今後の主戦場は単なるテキスト生成ではなく、「モデルの推論と思考ログ」に「Leanのような形式検証」を組み合わせ、ハルシネーションをゼロにする実用フレームワークに移ったと見てよいでしょう。

数学という厳密性の極致でこの仕組みが成立した意味は大きいです。同じ手法が新薬開発や材料設計などの隣接領域へ波及したとき、基礎科学の進展スピードはこれまでの比ではなくなるはずです。