OpenAI が10月6日に公開した数学の原稿のうち3本を、本人が翌日に取り下げた。公開先の GitHub リポジトリ（openai/math）の更新履歴 history.md に記録がある（一次情報）。原因は符号の誤り1つだった。この誤りが、ホッジ予想に近い主張を含むほかの原稿にも波及し、3本がまとめて崩れた。
原稿は722本（結果のまとまりで372）あり、約4,000問を解かせた成果として一度に出された。そのうち3本は、全体から見ればわずかである。それでも、この取り下げには大きな意味がある。外部の数学者がまだ読み終えていない段階で、出した側が誤りを見つけた。しかも、多くは Lean で形式化してあるという触れ込みが付いていた。
1つの符号から、主張が連鎖して崩れた
数学の結果は、ほかの結果を土台にして積み上がる。1本の原稿で符号を1つ取り違えると、その補題を使うほかの原稿も足場を失う。今回は、ホッジ予想に近い主張を含む原稿までがその連鎖に入った。ホッジ予想は、クレイ数学研究所のミレニアム懸賞問題の1つである。
人間の研究者が1本ずつ論文を書くなら、こうした依存関係は著者の頭の中にあり、査読者も一続きで追える。今回は数百本が同時に出ており、どの原稿がどの原稿に頼っているかを外から追うのは難しい。誤りの1か所が何本に及ぶのかを最初に知りうるのは、全体を持っている OpenAI だけである。それが分かったのが公開の翌日だった。量の多さが、そのまま検証の難しさになっている。
『多くは Lean で形式化済み』をどう読むか
OpenAI は公開の際、証明の多くを Lean で形式化してあるとしていた。Lean で形式化した証明が通っていれば、符号の誤りのような食い違いは機械が拒むはずである。それでも、取り下げは起きた。
このことから言えるのは、次のどちらかである（ここは本紙の推論）。1つは、取り下げた3本の要の部分が、そもそも形式化されていなかったこと。もう1つは、形式化された命題が、原稿に書かれた主張とずれていたことである。どちらであっても、『多く』という言い方では、どの結果のどこまでを機械が確かめたのかが分からない。読み手が知りたいのは原稿ごとの内訳だ。形式化の範囲がどこまでで、Lean の命題が原稿の主張と一致しているのかを、誰が確かめたのか。それが示されるまでは、722本のどれについても、形式化されていることを正しさの保証として扱うことはできない。
形式検証は、人間の検証が追いつかない量をさばくための切り札として語られてきた。今回の件は、その切り札がどこまで効いているかを、出す側が原稿ごとに示さなければ意味がないことを示している。
成果の速さに、検証が追いつかない
報道によれば、1つの結果に使った計算は ChatGPT Pro 並みで約3時間である。一方、専門家が新しい証明を読んで確かめるには、ふつう数週間から数か月かかる。Scientific American は、Andrew Sutherland が『モデルが公開されるまで、単一のエージェントの主張は未検証として扱うべきだ』と述べたと伝えた（二次情報）。Terence Tao は、このペースを『常軌を逸している』と言ったと伝えられる（二次情報）。
数学の共同体は、すでに受け皿づくりを始めている。Tao のブログには10月7日に『AHM statement on OpenAI's October 6 release of mathematical documents』が、10月8日に『What should we tell our students?』が載った。LessWrong でも『Are OpenAI's math results creative in an important way?』という問いが立てられている。これに先立ち、Erdős 問題のサイトは AI が出した説明のない証明を受け付ける窓口を絞った。LLM の助けを借りた結果を集める Hexagon も、投稿を最初は1日1本に制限している。どれも、1日に出せる量と1日に確かめられる量の差を、仕組みで埋めようとする動きである。
OpenAI の公開は、IAS が受け入れている数学と AI の諮問グループ（AGMAI）の助言を受けたとされる。ただ、AGMAI の任務は公開の進め方への助言であり、個々の証明を検証することではない。722本を一度に出せば、検証の負担は外の数学者に回る。今回の取り下げで、その負担が現実のものであることがはっきりした。
残りの原稿をどう読むか
4次元の掛谷予想や、リーマン予想に関わる進展といった大きな主張は、今も残っている（いずれも報道ベース）。今回の取り下げは、残りが誤っていることを意味しない。誤りを見つけて自分で引っ込め、履歴に残したことは、むしろ誠実な対応である。
それでも、読み方は変える必要がある。1日で3本が崩れたのなら、残る数百本も、外部の数学者が確かめるまでは OpenAI の『主張』として扱うべきだ。形式化については、どの原稿のどの定理を、どの命題で Lean が確かめたのか、内訳が出るのを待ってから判断すべきである。どのモデルがこの成果を出したのかも、まだ説明されていない。量の多さを、正しさの証拠として読むことはできない。
