OpenAIは10月6日、GitHub上に722本の数学論文を公開した。名も価格もAPIも明かされない社内フロンティアモデルが生成したもので、機械検証できるLean証明も添えられている。ただし独立した検証はまだ行き届いていない。
OpenAIの722本の数学論文とは何か
10月6日、GitHubに openai/math というリポジトリが現れた。同じ日にOpenAIは「Sharing AI progress in mathematics」という記事を出している。中身は722本の数学原稿で、372の研究ファミリーに分類されている。
書いたのは、名前も価格もAPIも公表されていない社内のフロンティアモデルだ。OpenAIによれば、これらの結果は数学と理論計算機科学の重要な未解決問題を解いたか、実質的に前進させたという。
むしろ見るべきは付属品のほうだ。多くの証明がLeanという、数学の証明をコンピュータで検証できるプログラミング言語で形式化されている。ただしOpenAI自身の説明は慎重で、モデルが原稿の準備と証明の形式化を助けたこと、正しさに責任を持つこと、数学的な論証そのものはシステムが生成したことを明記している。
「名前のないモデル」が意味するもの
今回いちばん異例なのは、モデルの名前も提供条件も示されていない点だ。通常、フロンティアモデルの成果は、そのモデルの宣伝とセットで発表される。今回は逆で、結果だけが先に出て、モデルは伏せられている。
これは何を意味するか。一つは、まだ公開できる段階にないモデルだということ。OpenAIは記事の中で、この結果を生んだモデルを「責任を持って公開するため準備中」と述べている。もう一つは、評価の焦点がモデルから成果そのものへ移っていることだ。読む側は、どのモデルが解いたかではなく、解が本当に正しいのかを問うことになる。
平均的な結果は、ChatGPT Proの思考をおよそ3時間使った計算量に相当するという。この数字は、1本あたりにどれだけの計算を投じたかの目安になる。
OpenAIの数学成果をどう検証するか
検証は一様ではない。OpenAIは独立した検証を外部に委ねておらず、Leanによる機械検証も、誰もが実行して確かめたわけではない。さらに報道では、OpenAIがNavier-Stokes（ナビエ・ストークス方程式）のミレニアム懸賞問題に対するAI生成の解答を、Lean証明付きで同時に公開したと伝えられている。
数学者にとって、この種の発表は受け止め方が分かれる。Leanの証明が通れば、論理の穴は機械的に潰せる。だが形式化の前提や定義の選び方に問題があれば、見かけ上正しくても意味が変わる。原稿の数学的な主張と、形式化された部分は、必ずしも同じ範囲を覆っていない。
OpenAIは今回、透明性のためにと、モデルの推論の要約10本、ChatGPT Pro換算の計算量の見積もり、試行した問題数の統計もリポジトリに載せている。未知の部分を減らす努力は見えるが、独立検証の不在という穴は残る。
数学者コミュニティへの影響
反応は複雑だ。OpenAIは、結果の出し方について独立機関である「Institute for Advanced Studyの数学とAIに関する諮問グループ」と協議し、その勧告を踏まえたと説明している。この手順は、大量のAI生成結果をどう公開すべきかという、業界共通の宿題に一つの型を示した。
研究の現場では、検証の人手が追いつかないという現実がある。722本の原稿を、専門家が1本ずつ丁寧に読むのは簡単ではない。AIが大量の成果を出せば出すほど、人間側の検証能力がボトルネックになる。この非対称は、数学に限らず科学全体でこれから強まっていく。
OpenAIは、AIが生む主要な成果を理解するためのワークショップや会議、特別プログラムに出資するとしている。発表だけで終わらせず、読み解きの場を用意する姿勢だ。
OpenAIの数学リリースで次に追うべき点
読み手が今できるのは、結論を急がず、検証の進行を追うことだ。見るべきは三つある。Lean証明のうち、どれだけが第三者に実行され通ったか。原稿の数学的主張と形式化の範囲がどこまで重なるか。そして、この結果を生んだモデルがいつ、どんな条件で公開されるか。
722本という数は圧巻だが、数は正しさを保証しない。名前のないモデルの成果をどう検証するかが、これからのAIと数学の関係を左右する。
