OpenAI、未公開モデルの数学論文722本を公開　「Lean」の検証はまだ一部

米OpenAIは2026年10月6日、社内で開発中の未公開モデルが数学の未解決問題に取り組んで書いた論文722本を公開した。証明の一部は、コンピューターが正しさを検査できる言語「Lean」で書き直して添えた。ただし形式化が済んでいない論文もあり、正しさの確認は数学者に委ねられた。AIが一度に大量の成果を出す時、確かめる工程が追いつくかが問われている。

722本の論文を一度に公開した

公開先は、誰でも読める数学の成果のリポジトリ「openai/math」だ。説明文によると、722本の論文を、主な結果と関連する議論や別証明ごとにまとめ、372の「ファミリー」に分けて収めた。論文のPDFとソースファイル、引用の情報、証明のコードが並ぶ。ライセンスはApache 2.0を採った。

成果の大半は、1つの未公開モデルが同じ手順で出したという。モデルには約4000問を与え、結果1件あたり平均で、ChatGPT Proの思考時間にして約3時間の計算を使った。10件には、モデルの推論の過程を要約した記録も付けている。題材は円周率の無理数度から量子ハイゼンベルク強磁性体、NP困難性まで幅広い。

機械で確かめた証明はまだ一部

証明の検査に使うのは「Lean」だ。数学の証明をプログラムのように書き、その正しさをコンピューターが検査できるようにする言語である。リポジトリには形式化した証明のライブラリと、証明と論文の対応をまとめた一覧があり、検査の道具「Comparator」の使い方も載る。

ところが、形式化はすべての論文に及んでいない。説明文は、多くの論文を形式化したがすべてではないと書き、形式化していない結果には問題が含まれる可能性があると認めた。問題が見つかれば速やかに直し、訂正は新しい版として記録して、以前の版も読める状態で残すという。

数学者の側が公開の作法を示す

OpenAIは9月21日、数学者が成果の扱いに意見を言う場として、独立した諮問グループの設立を発表した。諮問グループの設立を伝えたTechCrunchの記事によると、グループは米プリンストン高等研究所(IAS)に置かれる。グループは、OpenAIが社内の研究を進める速さについては助言しない。IASも、AI企業の意思決定の権限は持たないと説明した。発表の時点でOpenAIは、社内モデルが100を超える未解決問題を解いたと主張していた。

グループは9月29日、600を超える回答を踏まえてAIが生んだ数学を公開する際の指針を出した。指針はAI企業に、モデルの名前、使ったプロンプト、要約した思考の過程、かかった時間、計算の推定費用の開示を求める。同じ種類の問題で失敗した割合の報告も挙げた。形式化はComparatorで照合する課題ファイルなど決まった形式で示し、遅れる時はその状況をはっきり書くよう求めている。AI企業が管理しないリポジトリへの寄託、関連研究の引用、人が理解するための資金面の支援、公開中のモデルを広く公平に使えるようにすることも並ぶ。

今回のリポジトリは、計算時間と10件の推論の要約を載せる。モデルの名前は書かれていない。グループは10月6日の今回の公開を受けた声明で、これを「数学にとって重要な出来事」と呼びつつ、公開は人が理解する過程の「始まりであり、完了ではない」と述べた。指針が守られたかを判断するのは数学界だとしている。

確かめる手間が次の課題になる

TechCrunchの記事によると、OpenAIは諮問グループの発表の前に、数学の「ミレニアム懸賞問題」の1つであるナビエ・ストークス方程式の問題の解を公開していた。公開したリポジトリ「NavierStokesAndEuler」は、ナビエ・ストークス方程式とオイラー方程式の有限時間の爆発に関するLeanの形式化を収める。同じ記事は、フィールズ賞の受賞者25人が、AI企業が有名な問題の解決を競う動きを公開書簡で批判したと伝えた。諮問グループのうち、この書簡にも署名したのはCamillo De Lellis氏の1人だけだという。

今回公開された論文は722本に上る。諮問グループの声明は、その公開を人が理解する過程の始まりと位置づけた。つまり、正しさを確かめ、意味を理解して数学の知識に組み込む工程は、まだ人の手に残る。AIが一度に大量の成果を出す時、確かめる工程が追いつくかが問われている。

編集部の見方

編集部は、今回の公開で参考になるのは解いた問題の数より、成果に検査の材料と状態を添えて出した形だと見る。AIが出す量が増えるほど、人がすべてを読んで確かめるのは難しくなる。機械で検査できる証明、形式化の有無の明示、以前の版を残す訂正は、確かめる工程を仕組みに組み込む方法だ。計算時間と推論の要約は数学者の指針の求めに沿うが、モデルの名前は無い。エージェントで開発する読者も、生成したコードのどこまでをテストや型検査で確かめ、どこを人が読むかを分けて示せているかを見直すとよい。形式化のない論文の正しさは、まだ数学者の検証を待つ段階にある。