OpenAIが数学論文722本を公開、次のボトルネックは検証だ

OpenAIは、722本の数学原稿を372の成果群に整理して公開した。約4,000件の未解決問題を対象にした評価から生まれ、同社によれば1成果あたりの計算量はChatGPT Proの思考時間で平均約3時間に相当する。数学界にとって重要なのは量だけでなく、社内モデルがそれを生み出した速度でもある。

1回の評価から722本の原稿が生まれた

公開リポジトリには論文、補助的な証明資料、Leanによる形式化が収録されている。情報源となったZvi Mowshowitzのまとめは、主要な未解決問題500件のうち90件を解いた出来事として扱う。一方、リポジトリ自体は難易度の単一ランキングではなく、722本の原稿を関連する372群に分ける、より厳密な数え方を採用している。

OpenAIはモデルの推論過程を短くまとめた資料も10件公開した。ただしモデル自体は社内にとどまる。研究者は完成した文章と一部の形式的資料を調べられるが、同じシステムで全工程を再現することはできない。

証明の生産速度が研究者の読解力を追い越した

数学研究を制約するのは証明を見つける力だけではない。内容を理解し、検査し、既存研究の中に位置づける時間も必要だ。722本という規模は、候補となる成果の数と、責任を持って評価できる専門家の数との比率を変える。

実務上の影響は、個別の証明が審査に耐えるかどうかにとどまらない。研究所は生成と同じ真剣さで、形式化、独立検証、明快な解説にも資金を投じる必要がある。そうしなければ、発見の高速化は未確定な主張の待ち行列を長くするだけだ。

Leanがカバーするのは公開コレクションの一部だけだ

公開カタログによると、722本のうち主結果が形式化されている原稿は162本だ。372群のうち235群には何らかのLean資料が付くが、全原稿の完全な形式検証を意味しない。Leanが確認するのは入力された形式命題であり、それが非形式的な本文と正確に一致するか、成果が新しいか、重要かまでは単独で判断しない。

形式化されていない結果には誤りが残る可能性があり、コレクション全体も通常の査読を終えていない。歴史的転換だと即断するのは早い。それでも規模と検査可能な資料の多さを考えれば、単なる製品デモでは片づけられない。

独立した修正と再利用が価値を決める

最も重要な指標は公開された改訂履歴になる。独立した数学者が主要主張をいくつ確認し、いくつ修正し、後続研究がいくつ利用するかを見るべきだ。さらにOpenAIが形式化、より完全な工程記録、モデルへのアクセスを追加し、システムの能力と成功例の選別を切り分けられるかも重要になる。

今後数か月で引用される証明や新しい道具に育てば、研究の運営方法は変わる。大半が読まれないままなら、この公開が示す最大の事実は、数学が主張を吸収する速度より速く主張を生産できるようになったことだ。

Lilithの判定

OpenAIは数学者に722個の封印された荷物を送り、その一部にだけ検査機を添えた。歴史が動くのは、独立した研究者が中身を開け、確かめ、実際に使った時だ。