OpenAI、AIが書いた数学論文722本のうち3本を符号ミスで撤回

OpenAIは2026年10月6日、未公開のAIモデルが書いた数学の原稿722本を公開し、翌日にそのうち3本を撤回した。GitHub上のOpenAIの改訂履歴によると、符号ミスが1つの証明の重要な段階を壊した。ほかの2本の論文は、その証明に依存していた。この件は、AIが書いた研究を大規模に検証することの難しさを示している。数学者たちがこの公開をめぐって議論している理由でもある。

OpenAIが公開したもの

ファイルは、openai/mathという公開GitHubリポジトリにある。Implicator.aiは「結果ファミリー」を372、原稿を722と数えている。Fortuneは、この公開を370を超える未解決問題へのAIによる完全または部分的な解答と説明している。これは別のものを数えているので、2つの数字を混同してはならない。

Implicator.aiとYahoo Techは、この成果がOpenAIの未公開の社内モデルから出たと伝えている。Implicator.aiによると、OpenAIは評価の間に約4000問を出題した。結果1件あたりのChatGPT Proの計算時間は、平均で約3時間だった。広報担当者は、ほぼすべての結果が1つのAIエージェントへの1回のプロンプトから生まれたと述べた。

Fortuneによると、OpenAIはミレニアム懸賞問題（Millennium Prize）7問のうち、さらに3問でも進展があると主張している。これらは賞金100万ドルがかかった有名な未解決問題だ。完全な解答はまだない。OpenAIは数週間前に、ナビエ・ストークス方程式（Navier-Stokes）の問題を解いたと主張していた。この主張には、数学者たちが反論した。

3本の撤回

10月7日付の改訂履歴には、撤回された論文が載っている。

Paper	役割
Algebraicity of Weil classes on split abelian eightfolds	誤りを含んでいた
Algebraicity of Kuga-Satake Correspondences for K3 Surfaces	それに依存していた
The rational Hodge conjecture for products of K3 surfaces	それに依存していた

理由は「符号ミスにより、安定化トレースの打ち消しの議論が成り立たなくなる」と記されている。履歴には、OpenAIがほかの14本の原稿を修正したとも書かれている。13本は、改訂された関連論文を引用するよう更新された。撤回された版は注意書きつきで公開されたままだと、Implicator.aiは伝えている。

誰が誤りを見つけたのかは、どの情報源も述べていない。OpenAI自身のページにも書かれていない。

どこまで検証されたか

Leanは、証明の論理の各段階をコンピューターに確認させられるプログラミング言語だ。Implicator.aiと改訂履歴によると、残る719件の主要な結果のうち300件にLeanによる形式化があり、約42%にあたる。Fortuneは、形式的な検証があるのは「一部」の問題だけだと述べている。Leanの検証が確かめるのは論理であり、結果が新しいか重要かどうかではないと、Yahoo Techは指摘している。

モデルは利用できないため、外部の人間は再実行できない。Implicator.aiによると、OpenAIはプロンプトを公開せず、平均の計算量だけを示した。Institute for Advanced Studyの諮問グループは、9月29日にさらなる情報開示を勧告していた。Fortuneによると、OpenAIはその助言に一部しか従わなかった。

数学者たちの意見

FortuneとImplicator.aiによると、反応は割れている。

• University of TorontoのDaniel Littは、この公開を「数学にとってすばらしい」と評した。論文を伏せておく理由は見当たらないとも述べた。
• New York UniversityのTristan Buckmasterは、デューデリジェンスに疑問を呈した。発言はNew York Times経由で引用されている。
• MITのAndrew Sutherlandは、「1つのエージェントで問題を一発で解いたという主張は、すべて未検証として扱うべきだ」と述べた。
• IASの諮問グループは、「この公開は人間が理解する過程の完了ではなく、始まりである」と述べた。

Implicator.aiは、ある食い違いも指摘している。広報担当者の「1回のプロンプト、1つのエージェント」という説明は、ナビエ・ストークスの結果に使ったとOpenAIが述べた1万のエージェントと矛盾する。

開発者にとっての意味

コード、証明、研究にAIを使う人は誰でも、同じ検証の問題に直面する。

• 生成と検証を分けること。 Leanによる検証は、読むだけでは見つからなかった誤りを捉えた。AIの出力に機械で検証できる形があるなら、テスト、型、証明などを、誰かが信用する前に実行すること。
• AIの出力どうしの依存関係を追うこと。 1本の誤った論文が、ほかの2本を巻き込んだ。生成した成果物のどれがどれに基づいているかを記録しておくこと。
• 入力を求めること。 プロンプトとモデルへのアクセスがなければ、信頼できる手法と幸運な結果を見分けられないと、Yahoo Techは指摘している。頼りにするAIの主張には、背後にあるプロンプト、設定、ログを求めること。
• 撤回を普通の出来事として扱うこと。 2日間で722本のうち3本というのは、警戒するほどではない。明確な改訂履歴を公開した点こそ、見習うべきところだ。

注目すべき数字は、形式的な証明がある結果の割合だ。現在の42%は、この公開のうちどれだけを数学者が手で読む必要があるかを示している。