OpenAIが数学論文722本を公開、検証はこれから始まる

OpenAIは、722本の数学論文を372の研究系列にまとめて公開した。未公開の社内モデルを約4,000件の未解決問題で評価した際に得られた成果で、同社によれば1件あたり平均3時間のChatGPT Pro thinking計算資源を使った。

単発の成果発表ではなく722本の公開資料になった

公開リポジトリには、論文、ソースファイル、引用方法、証明を支える資料が収録されている。選ばれた10件には、モデルの推論過程を短くまとめた文書もある。OpenAIの発表ページは検証時に閲覧できなかったため、本稿は同社の公開リポジトリとその説明文書に基づいている。

成果はそれぞれ異なる検証段階にある。OpenAIは、すべての論文にLean形式化が付いているわけではなく、形式化されていない成果には誤りがあり得ると明記した。修正履歴と過去版も保存する方針だ。

数学界が受け取ったのは画期的成果の順位表ではなく目録だ

研究者にとって最大の問題は規模である。数百本の論文について、正しさ、重要性、独創性、先行研究との関係を調べるには、生成に要した時間を大きく上回る専門家の労力が必要になる。722という数字だけでは、査読を通過する成果の数は分からない。

Leanは、形式言語へ移された証明の論理的な正しさを検査できる。しかし、その結果が新しいか、重要か、別名ですでに知られているかまでは判断しない。OpenAIは評価作業の一部を、社内benchmarkから公開の数学コミュニティへ移した形だ。

3時間の計算資源は専門家の検証を代替しない

1件平均3時間という数字が示すのは生成費用であり、知識として確立する費用ではない。実際には、前提の確認、先取権の調査、原稿の修正、既知の定理を新しい包装で示しただけかを見分ける専門家の時間が必要だ。

リポジトリにある57,328個のLeanファイルも、57,328件の独立検証済み発見を意味しない。これは大規模な補助資料群の一部であり、OpenAI自身も形式化が未完了だと説明している。

独立した評価と修正履歴が成果の価値を決める

今後の重要な指標は、独立した数学者が新規性と正しさの両方を認める研究系列がいくつ現れるかだ。同時に、今後数か月で修正、撤回、Lean形式化の追加がどれだけ発生するかも見る必要がある。

リポジトリは旧版を保存すると約束している。変更履歴が読みやすく保たれれば、モデルの能力だけでなく、大量生産された数学的主張を整理する費用も可視化される。

Lilithの判定

OpenAIは数学者の前に722本の論文を積み上げた。黒板を埋める反論に耐えるものと、赤鉛筆で消えるものを分ける作業はここからだ。