技術分解 019｜openai/math：OpenAI が一括オープンソース化した 722 件の AI 数学原稿のリポジトリ分解

10 月 6 日、OpenAI は GitHub でリポジトリ openai/math を公開し、未発表の内部モデルが生成した数学の研究成果を一括公開した：722 件の原稿、372 個の結果族、3.1 GB、132,880 個のファイル、2 日間で 9832 スター（依然増加中）、HN（Hacker News）関連の議論で 1200 超のアップボート、1400 余りのコメント、公式ブログ『Sharing AI progress in mathematics』も同日公開された。これは論文のコレクションではなく、「原稿＋形式化＋検証ツール」の3点セットであり、このリポジトリの読み方、検証方法、そして論争は、ほぼすべてこの3層構造に根ざしている。本稿では6つの事項に沿って分解する：何であるか、なぜ見る価値があるか、構造とメカニズム、数字と境界、どう検証するか、価値判断。

一、それは何か

openai/math は AI 数学成果リポジトリである：主言語は Lean、Apache-2.0 ライセンス、3層のコンテンツに加えて1部の原稿マップを備える。

第1層 preprints/ は、722個のディレクトリからなり、1ディレクトリにつき1部の研究原稿が含まれ、内部には paper.pdf、LaTeX ソースファイル、引用およびビルド説明が含まれる。ディレクトリ名には日付が付されており、最も早いもので9月10日——まさにナビエ-ストークス（Navier-Stokes）の結果が対外発表された日である——最も遅いもので10月5日、そして公開は10月6日となっている。原稿は約1ヶ月間蓄積された後に一括で公開され、最初のコミットのタイムスタンプも公開当日になっている。

第2層 lean/ は、形式化ライブラリである。OAI/ 配下では学科ごとに24個のサブディレクトリに分かれており、Algebra から Topology まで、12.17万個の .lean ファイルが存在する。mathlib4 に依存し、特定のコミット d13f23b にロックされており、patches/ には上流へのパッチが格納されている——このライブラリは単に mathlib4 を消費するだけでなく、上流に改変を加えている。

第3層 reasoning_traces/ は、10個の結果族の推論要約 PDF である。README では abridged summaries と自称しているが、HN（Hacker News）のコメントでは、より正確な表現は「要約の抜粋」であると指摘されている——元の推論軌跡ではない。

最上位層のナビゲーションは2部からなる：CONTENTS.md は640 KB の原稿マップであり、722部が逐一登録され、それぞれに題目と結論の参照先が示されている。後文で引用する 001、003、102、180 はこのマップ内のエントリ番号である。overview.pdf はソースファイルを伴い、323 KB で、全結果のガイドである。リポジトリは「族」ごとに編成されており、1つの主結果に付随する論証、推論、代替証明を加えて1族とみなす。722部の原稿は372個の族に分類されている——相当数の結果が代替証明や付随する論証とともに公開されており、読む際は篇単位ではなく族単位で読む方がお得である。

二、なぜ今注目すべきか

第一の理由は、結果リスト自体の重みである。722件は722の孤立した問題ではなく、族ごとに編成されたそれは、むしろ一つの研究アーカイブに近い。CONTENTS.mdには重量級の項目のほか、πの無理性指数、Erdős型算術級数擬多項式界、Kaplansky直有限性特性2反例、自由群因子同型、相対論的Vlasov–Maxwell、Mahler予想、量子Heisenberg強磁性体自発磁化が散在している——数論、グラフ理論から数学物理学に至るまで。重量級の中から4件を選んで述べる。

003番、準リーマン予想：ζ関数とすべてのDirichlet L関数がRe(s)>7/8の領域で零点を持たないこと、ならびにLandau–Siegel零点の一様排除。方向性を先に明確にしておく必要がある：零点自由領域は右に寄るほど強く、人類の記録は11/12≈0.9167であり、7/8=0.875はその左側にある——これは当該システムが古い問題において独立に押し進めた下界であり、記録更新ではない。

102番、Unique Games予想（Khot、2002）、原稿は成立する証明を与えている。理論計算機科学のインフラストラクチャ級の命題であり、大量の近似不可能性結果がそれを前提としている。HN（Hacker News）では、ある千禧年問題よりも重みがあるというコメントも見られた。

180番、Barnette予想（1969）：すべての有限単純3次2部平面3連結グラフはハミルトン閉路を持つ。グラフ理論における57年間の懸案であり、HNのユーザーが、当時の最強モデルを使ってこの問題に数ヶ月取り組んだが成果がなかったと述べている。

001番、Milne有理性予想（アーベル多様体）、同じ項目にHodge予想のCMアーベル多様体という特殊な場合の証明の主張が並記されている——ここで明言しておくべきこと：特殊な場合の主張にすぎず、クレイ数学研究所の認証は発生していない。

第二の理由は、公開の形態である。これまでAI数学の公開は単点の主張が多かったが、722件を一括で公開し、形式化レイヤーと検証ツールを内包したリポジトリ全体を提供するという形態は、それ自体が稀である。HNの議論ではすでに新しい遊び方が登場している：リポジトリ全体を自身のエージェントに投げ込み、各原稿のsignificance（重要性）に逐次回答させる者もいる——722件というスケールが、新しい読み方を生み出しているのである。

三、核心技術メカニズム

生成パイプラインについて、README には次のように記されている。圧倒的多数の結果は、同一の未公開内部モデルによって固定プロセスで生成された。全程で約 4000 問が投入され、結果1件あたり平均3時間の ChatGPT Pro 相当の思考計算量を消費した。生成結果は族に集約され、有意性の閾値を通過した後、722 件が残った。2項目が固定プロセス外の例外として挙げられている。リーマンゼータ零点自由領域と CM アーベル多様体の Hodge 場合であり、その差異について README は詳述せず、零点自由領域の論文が人工的な編集・推敲により可読性を高められたとだけ説明している。

形式化レイヤーの構成は詳細に見る価値がある。lean/docs/ 配下では、各形式化結果につき1ページのドキュメントがあり、適用範囲、対応する論文、および Comparator リンクが明記されている。引き続き 003 号を例に挙げる。ステートメントは ζ 関数、すべての Dirichlet L 関数、および Q(√-3) 上の有限階 Hecke L 関数をカバーしている。主指標の s=1 における極はステートメントから明示的に除外されており、定数には陽な値は与えられていない。何が形式化され、何が形式化されていないかがドキュメントで明確に区別されている。このリポジトリを読む際は、コードの前にまず docs を読むべきであり、この各ページの説明こそが最も労力を省く入り口となる。

推論要約レイヤーについては、あえて冷水を浴びせておく必要がある。10個の族には reasoning_traces が付属しているが、README の表現では “abridged summaries” となっており、HN での議論ではこれが実際には「要約の抜粋」であると指摘されている。「結果1件あたり平均3時間」という思考量と対照的に、コミュニティの手元に提供された推論資料は、モデルの推論パスを再現するには程遠い。「モデルがどう思考しているか」を研究したい人にとって、これはリポジトリで最も不透明なレイヤーである。

検証の階層化はメカニズムの中で最も重要な一環である。formalization.yaml では、主結果が形式化された論文が 162 編集計されており、722 件の2割強を占めている。README の原文では、結果は異なる検証段階にあり、すべてに Lean 形式化が付随しているわけではなく、未形式化の部分には誤りが含まれる可能性があると自認している。言い換えれば、リポジトリ自らが信頼性をグラデーションとして示していることになる。162 編は機械検証可能であり、残りの 560 件は人間可読な主張に過ぎない。

四、数字と境界

数字の全容：722件の手稿、372の族、162件の形式化、132,880個のファイル、3.1 GB、約4000問の投入、1結果あたり平均3時間、2日で9832スター；Leanライブラリに24個の学科サブディレクトリ、12.17万個の .lean ファイル。

境界について4点を挙げる。

第一に、方向を読み間違えないこと。7/8は11/12より弱く、AIの零点自由領域の結果は人類を超越したものではない。「記録破り」と書くのはこのトピックで最もよくある間違いであり、方向を書き間違えると、記事全体の信用まで失われる。

第二に、形式化はエラーがないことを意味しない。Leanによる検証の前提は、定理の陈述が正しく翻訳されていることである——機械がチェックするのはコード内のその陈述であり、論文内の中国語や英語の結論ではない。HNの高評価の疑問はまさにここにある：24の学科にまたがっており、各陈述の翻訳はすべて人間の目による確認に値し、003号文書で定数に明示的な値が与えられていないことなど、まさにこの種のチェックで突き詰めるべき細部である。失敗すると直接予測する人もいれば、応答側はREADMEで既に未形式化部分にエラーがある可能性を自認していると指摘した。

第三に、公開は認証と同義ではない。ブログのタイトルにはsolvingではなくsharingが使われており、クレイ認証もピアレビューも行われていない。論文の署名はOpenAIであり、人間の査読者の署名はない。HNでのGitHubとarXivの論争もここから生じた：GitHubでの公開がペイウォールを打破したと称賛する人もいれば、数学者は数学の成果は本来arXivに流れるものだと反論した。リポジトリのアーカイブ価値と論文のアーカイブ価値は同型ではない。

第四に、計算力の尺度は背後を見る必要があり、スター数の尺度は対象を見る必要がある。3時間は平均値の尺度であり、HNでAlphaZeroの旧い話を掘り出す人もいた——「4時間の超人」は実際には4時間×5000台のTPUである——これは「3時間のChatGPT Proと同等」といった表現には背後の総量を問うべきだと注意を促すものである。一方、2日で9832スターというのは関心度を測ったものであり、正確さではない——リポジトリ自身でさえ722件を検証進捗と表示しており、コミュニティによる再検証はまだ始まったばかりである。

五、どう動かすか、誰が使えるか

モデルを動かさなくても検証できる、これがリポジトリの設計において最も実質的な部分である。lean/READMEはComparatorのフローを示している：まずcomparator、landrun、lean4exportの3つをインストールし、lake updateで依存関係を引き上げ、lake exe cache getでmathlib4のキャッシュを取得し、その後lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.jsonを実行する——これで003番の形式化陈述に対して照合チェックを行う。ComparatorChallenges/の中には公式にプリセットされたチャレンジリストがあり、このフローに従えば項目ごとに抜き打ちチェックができる。ライブラリ全体をコンパイルする場合、READMEではLinuxデフォルトのvm.max_map_countの上限では足りない可能性があると特に警告しており、CMake -DMMAP=OFFにGLIBC_TUNABLESを加える回避策を提示している——リポジトリが大きすぎて公式がわざわざコンパイルの罠回避説明を書くほどであることは、まさにそのボリュームの注釈となっている。

対象者を3つのタイプに分けて説明する。Leanと形式化数学を行う人：対照論文とドキュメント付きの162件の形式化結果に、mathlib4のロックとパッチが加わっており、直接読んで直接検証できる資産であり、「AI（人工知能）の成果がどのようにLeanに落とし込まれるか」を観察するための既成サンプルでもある。理論計算機科学を行う人：Unique Games（一意ゲーム予想）のあの原稿は、最終的に成立するかどうかにかかわらず、行ごとに読む価値がある——それが牽引する非近似性の版図が大きすぎるため、結論を検証する各ステップが学界で繰り返し引用されることになるからだ。モデル評価を行う人：4000題の投入、族の集約、有意性の閾値という一連のスクリーニングパイプラインは、各結果につき3時間というコスト基準とともに、希少な一次手法論の素材となっている。

ただ見物したいだけの人にとって、ハードルはディスク容量と忍耐力である：3.1 GBのcloneに、うまく通るとは限らない全ライブラリのコンパイルが加わる。何もインストールしたくない人は、まずトップレベルにある323 KBのoverview.pdfを読むこと。20分でリポジトリ全体の結果について地図感を把握してから、どの学科のディレクトリに進むかを決めればよい。

六、価値判断と誰に適しているか

サンプルの価値は高い。それは「AIが数学を解くこと」を、プレスリリース上の単発の主張から、数え上げ可能、抜き取り検査可能、機械による再検証可能な公開リポジトリへと変えた。162という数字は特に重要である：仮に残りがすべて疑わしくても、この162篇の形式化されたステートメントは、コミュニティが独立して検証できる確固たる内容である。フィールズ賞（Fields Medal）受賞者の陶哲軒（Terence Tao）がMastodonで示した態度（HN（Hacker News）経由で引用）も同じ方向を向いている：AIが自身の結果を人間の数学者に説明できることを望み、AIが説明とコミュニティ構築においてプラスの貢献ができると考えている。

生産性の価値は人による。数学と理論計算機科学の研究者にとって、これは知っておくべき存在である。自分の課題が先を越されていないか判断するためだけでもそうだ——HN上ではすでに博士課程の学生が「論文を書きかけで722篇に先を越された」という焦りを示しており、共感からの返信で提案されたのは、最前線を受け入れ、未発表の研究の原文をAIに与えないことだった。この感情自体も業界の変数である。エンジニアリング側にとって、検証ツールチェーンとコンパイルの落とし穴回避ドキュメントは、大規模なLeanプロジェクトの既存の参考資料となる。結論だけを求める人には一言提醒しておく：ここには結論はなく、異なる検証段階における主張があるのみである。

ブログではさらに、一連のワークショップ、会議、専門プロジェクトへの資金提供を約束し、数学界がAIの産出した重大な結果を理解できるよう支援すると述べている。また、これらの結果を産出したモデルを責任を持ってリリースするよう推進しているとも述べている。READMEでも、コミュニティがホストするリポジトリを模索していることに言及している。最後に前段の経緯を補足しておく：8月の10題のLean、9月のフィールズ賞受賞者の声明と顧問グループの提案書が、今回のリリース方式の外部背景となっている。批判的な側面の展開については同日のホットトピック編で扱っているので、ここでは繰り返さない。

一言で判断すると：openai/mathの歴史的位置は、722件のうち最終的に何件が成立するかにかかわらず、AIの数学的産出を人間の数学が一つずつ検証できる軌道に初めて乗せたことによって決まる——スター数はOpenAIのものだが、一つずつ検証する権利はコミュニティのものである。

参照元

• リポジトリ本体：github.com/openai/math（ローカルで clone した後、README、CONTENTS.md、lean/ ディレクトリ、formalization.yaml、git log を項目ごとに比較；ビルドは一切実行せず）
• OpenAIブログ『Sharing AI progress in mathematics』（2026-10-06）
• HN story 49984923（2026-10-08 時点で1200超のUpvote、1400余件のコメント；テレンス・タオの表明および顧問グループの提案書はいずれもHNからの引用であり、原文を一字一句照合していない）
• スター数 9832★ は 2026-10-08 時点のデータであり、現在も増加中である