学術＆研究 - ACADEMICS & STUDY -

OpenAI、AIが生成した数学原稿722本を公開　翌日に3本を撤回、証明の検証資料も共有

:::small 画像：[OpenAI] ::: OpenAIは2026年10月6日（現地時間）、社内のフロンティアモデルが生み出した数学の新たな成果を[公開]した。GitHubで722本の原稿と証明の検証用資料などを共有したが、翌7日には証明の誤りを理由に3本を撤回した。10月9日時点の掲載数は719本となっている。 ## 数学の研究課題約4,000問から成果を整理 公開先の[「openai/math」]は、数学の原稿や証明を支える資料をまとめたリポジトリである。現在の719本は、関連する成果ごとに372のグループに整理されている。一つのグループには、中心となる結果に加え、その結果から導かれる性質や別の証明などが含まれるため、原稿数と解決した問題数は一致しない。 OpenAIは、従来の数学評価でモデルの成績が上限に達したことを受け、開発中のモデルを未解決の研究課題で評価する取り組みを拡大した。今回の評価では約4,000問を与え、得られた出力を重要性などに基づいて整理した。 成果を得るための計算資源は、平均で、この社内モデルを使ったChatGPT Proの思考時間約3時間分に相当するという。これは計算資源を換算した値であり、各問題が実時間で3時間以内に解かれたことを示すものではない。 公開した原稿は、数論、幾何学、解析学、理論計算機科学など幅広い分野にわたる。[準リーマン予想や、有理数上のヒルベルトの第10問題などに関する原稿]も含まれる。 ## 証明の検証資料も公開、翌日には3本を撤回 OpenAIは、多くの証明をプログラミング言語「Lean」で形式化した資料も公開した。Leanは、数学の証明をコンピューターで検証するために利用できる。モデルの推論をまとめた要約10件も共有している。 ただし、公開した原稿の検証段階は一律ではなく、すべてにLeanによる形式化が付いているわけではない。OpenAIも、形式化されていない成果には問題が残る可能性を認めている。 OpenAIは10月7日、証明で正負の符号を誤った原稿1本と、その証明に依存する原稿2本の計3本を[撤回]した。誤りが見つかったのはヴェイユ類に関する原稿で、撤回対象にはK3曲面に関する2本も含まれる。 **■ OpenAIが公開した10月7日の更新履歴。数学原稿3本の撤回と、ほかの原稿の修正、Leanによる形式化の追加を報告している** ![history.jpg] :::small 画像の出典：[OpenAI公式GitHub] ::: このほか14本について、証明の修復、主張の訂正、仮定や依存関係の明確化などを実施した。それに伴い、別の13本でも参照先や版の日付を更新した。主要結果が形式化されている原稿は300本で、719本の約42％としている。 撤回した原稿には問題点を説明する告知を付け、過去の原稿へのリンクを残している。修正版についても以前の版を参照できるようにした。 ## 数学者が成果を理解するための活動も支援へ 今回の公開方法には、高等研究所の独立した数学・人工知能諮問グループの助言と[公開提言]を取り入れた。 同グループは、AIが生み出した数学の成果について、先行研究の適切な引用や読みやすい証明の記述、人間が成果を理解するための支援を求めている。一方、科学者が利用できない独自モデルで高度な数学問題を試す慣行には、支持しない姿勢を示している。 OpenAIは、AIが生み出した主要な成果への理解を深めるため、ワークショップや学会、特別プログラムに資金を提供する予定である。成果を生み出したモデルの公開に向けた取り組みも進めているが、今回の発表では提供時期を示していない。 :::box [関連記事：OpenAI、GPT-6 Astra超えの未公開AIが現代数学の七大難問「ナビエ・ストークス方程式」の解決証明を生成　先行研究の扱いに数学者が異議も] ::: :::box [関連記事：「AI企業の難問競争は数学を損なう」フィールズ賞受賞者25人が声明　森重文氏ら] ::: :::box [関連記事：OpenAIの内部AIモデル、エルデシュの「単位距離予想」を反証　外部数学者が検証] ::: :::box [関連記事：Anthropic、未公開Claudeが「リーマン予想」に挑戦　証明は失敗も関連問題で41.6％→67.2％、「自分を信じて」と人間が励ます] ::: :::box [関連記事：フィールズ賞のテレンス・タオ氏、「GPT-5.2 Proが数学の未解決問題をほぼ自律的に解き切った」と評価──エルデシュ問題#728で示されたAIの新たな到達点] :::