トレンド追跡 015｜3ヶ月間非難されて、ようやく今回の公開に至る：OpenAI 722件の数学手稿に対する言行監査

まず時間を確定しておく。10月6日、OpenAIはブログ『Sharing AI progress in mathematics』を公開し、同日にGitHubでリポジトリopenai/mathを公開した——2日で9832個のスターを獲得し、この速度は学術系リポジトリとしては非常に稀である。対応するHacker Newsの議論は、10月8日午前時点で1241の支持票、1412のコメントを集め、依然としてトップで議論が展開中である。これは定例のオープンソース化ではない：8月から10月上旬まで、OpenAIの数学分野における公開方式は3ヶ月間連続して批判され、今回の大量公開はその批判の波の後に発生した——時間の順序そのものが、今回審査すべき対象なのである。今回の記事も、持続的に展開している事件の途中に書かれており、ランキングの位置はまだ変動しており、数値は10月8日午前を基準としている。以下の事実は公式ブログおよびリポジトリのREADMEを基準とし、HNの反応プールのデータは独自に照合し、転載部分は本文中で注記した。

何が起きたのか

OpenAIは内部モデルの数学的成果を一括公開した——722件の研究原稿、372の結果族に分類され、リポジトリは132,880ファイル、3.1GB、主言語は形式証明言語Lean、Apache-2.0ライセンス。

リポジトリは3層に分かれている。第1層はpreprintsで、722篇の論文のPDFとソースファイル；第2層はleanディレクトリで、12万のLeanファイルが24の学科に整理されており、コミュニティ数学ライブラリmathlib4の固定バージョンに依存している；第3層はreasoning_tracesで、10件の推論過程の要約の抜粋——公式自身の表現が「要約の抜粋」であり、完全な思考過程ではないことに注意。検証の入り口も用意されている：公式はcomparatorフローを推奨しており、comparator、landrun、lean4exportの3つのツールを環境に設定し、lake updateで依存関係を引き上げ、lake exe cache getでコミュニティのコンパイルキャッシュを取得すれば、結果族を1つずつ検証できる。これらの結果を生成したモデルは公開されておらず、公式の見解は「未公開の内部最先端モデル」である；このモデルは約4000問を解き、結果1つあたり平均3時間のChatGPT Pro相当の思考計算力を費やした。722篇のうち162篇にはLean形式化された主結果があり、残りの560篇は論文のみである。ブログでは同時に一連のワークショップへの資金提供を約束し、「これらの結果を生成したモデルの責任ある公開」を推進していると表明している——モデル自体がいつ公開されるかは、後続のための伏線となっている。リポジトリの内部構造や検証フローの実行方法については、同日の解説019で特集しているため、本稿では詳述しない；本稿の主眼は別のことにある：今回の公開がどのように叩かれて出てきたかである。

3ヶ月間叩かれて、ようやく今回のリリースに至った

まずはタイムラインを提示しよう。

8月、OpenAIはAstraモデルを使い、Lean言語で10問の数学問題のデモを行った——形式化ツール自体は数学コミュニティの公共インフラであるにもかかわらず、あるAI企業がそれをモデル能力のショーケースとして使ったことで、一部の数学者が初めて違和感を覚えた。9月10日、ナビエ-ストークス方程式に関する証明の主張が現れた——これは流体力学の百年の難題であり、査読されていない主張が直接一般公開されたため、その異様さは想像に難くない。9月11日、25人のフィールズ賞受賞者が共同声明を発表し、AI企業の数学分野におけるリリース方式を指摘した；前回我々はこの件について書いた（ホットトピック 003、9月12日）。9月中旬、数学者からのリリース方式に対する批判が報道され続け、焦点は単発のイベントからリリースメカニズムそのものへと移った。そして10月6日：ブログでは、今回のリリースは数学とAIの顧問グループの助言に沿って設計されたと述べられた。

この帰属チェーンで最も痛い点は、顧問グループの提言書そのものに隠されている。HN（Hacker News）の議論からの引用によると、プリンストン高等研究所に属するこの顧問グループ（AGMAI）の提言書は、冒頭で2つの意味を明記している：このようなやり方を支持しないことを明示し、専有モデル上で高度な数学問題をテストすることを停止するよう求めている。OpenAIの実際の行動と照らし合わせると、言行の監査結果は明確である：リリースの規範に関する半分——公開リポジトリの構築、引用規範の提供、Lean形式化の実施、推論要約の付加、計算能力スペックの標示——はすべて採用された；「テストするな」というもう半分については、ブログ原文でわざわざ段落を割いて、内部の最先端モデルで引き続き数学問題をテストすることがなぜ重要なのかを論証している。どうリリースするかは聞いた；テストするなとは聞かなかった。双方から半分ずつ取ったのだ。この選択自体が優先順位を物語っている：手続き的正義は話し合いの余地があるが、テストのペースは譲れない。ブログは今回のリリースを数学界との協力のサンプルと描写しているが、協力条件の中で最も動かせない一条——テストの停止——はどの段落にも現れていない。原稿締め切り現在、OpenAIは「テスト停止」という要請に対していかなる肯定的な回答も行っていない。フィールズ賞受賞者の陶哲轩（テレンス・タオ）はMastodonに投稿し（HNからの引用による）、共同声明よりも穏やかな態度を示した：彼はAIが人間の数学者に結果を説明できることを望み、またAIが闡明、コミュニティ構築、新たな研究方向において正の貢献をできると信じている——穏やかとはいえ、彼も同様に「どうぞテストを続けてください」とは言わなかった。

第3の層の批判は「機械検証可能」というセールスポイントに向けられている。162を722で割ると、形式化率は約22%である；残りの560篇はPDFのみで、Lean証明がない——言い換えれば、8割近くの原稿において、機械検証という保険が欠落している。そして形式化自体も安全通行手形ではない：arxiv 2610.08144の論文が指摘するように、自動形式化の忠実性判定問題はSCI階層においてSCI=∞であり、停止問題（SCI=1）よりも難しい——平たく言えば、ある機械翻訳が元の論文を忠実に復元しているかを判定することは、プログラムが停止するかを判定することよりも通用アルゴリズムが存在しないということである。すなわち、Leanが検証するのは形式化された後の陈述であり、この形式化が元の論文を忠実に翻訳していることを保証するものではない。HNでの同種の疑問は高評価を得た：Lean証明書の前提は定理の陈述が正しく翻訳されていることだが、これほど広範な分野にまたがってこの保証はない。リポジトリのREADME自体も認めている：形式化されていない部分には誤りがある可能性があり、できるだけ早く修正するとしている。3者の見解はここで珍しく一致している——公式、論文、コミュニティのすべてが検証の空白が存在することに同意しており、ただ公式がそれを免責段落として書いたに過ぎない。

コメント欄の声

HN（Hacker News）で1400件以上のコメントが寄せられ、いくつかの代表的な声があった。

最も多くの「いいね」を獲得したコメントは、OpenAIと数学界のやり取りに肯定的な評価を与えたものの、痛烈な条件を付け加えていた。それは「公開的に非難されてからようやく行った」ということだ。別の意見はさらに踏み込んでいた。数学界が求めてきたのは許可ではなく規範であるとし、以前のリリースプロセスが人間の研究者の方向性を先んじて発表したり、既存の研究の引用を漏らしたりしたと非難している（ディスカッション欄での転述による）。こうした積年の不満は、一度の大量リリースでリセットできるものではない。

リリースのチャネル自体についても議論があった。一部の人々は、公開リポジトリにLeanコードを加えることが数学の発表における新たなパラダイムだと考えた。一方、別の人々は、論文はarXivに投稿して同行レビュー（ピアレビュー）を受けるべきであり、GitHubはレビューに代わるものではなく、コードの存在感もレビュー手続きの欠如という問題を覆い隠すことはできないと主張した。同行レビューを信頼の基盤とする数学という分野において、チャネルを巡る争いは突き詰めれば信頼を巡る争いである。

最も人間味のあるコメントはPhD（博士課程）学生からのものであった。「書きかけの論文の方向性が722本の論文に被弾したらどうすればいいのか」というものだ。以下の共感は非常に直接的だった。「研究をAIに食わせてはいけない。訓練に使われ、先んじて発表されてしまうからだ」。署名の問題もここで提起された。722本の論文にはOpenAIとだけ署名され、具体的な研究者の名前がない。少なくとも査読者を署名させるべきだという提案もあったが、それに対する反応は「それは大衆に査読者ではなく機械を信頼するよう訓練するのと同じだ」というものだった。また、競争環境下ではチームのメンバーリストをそもそも公開しにくいという説明もあった。一つの署名欄に、3つの立場が入り乱れている。

また、広く出回った個人的な推測もあった。「今回の結果は数学における50〜100年分の進展に相当する」というものだ。ただし、これは1人のユーザーの推測であり、コンセンサスではないことに注意が必要で、コメント欄には反対の声も少なくなかった。この種の規模の判断については、急いでどちらかの側に立つ必要はない。リポジトリは公開されており、結果は数学界によって一つ一つ消化されていく。真価のほどは、時間が答えを出してくれるだろう。

一般ユーザーができる3つのこと

第一に、自らの手で定理を検証する。 リポジトリのドキュメントには完全な comparator フローが記載されており、lean/README の手順に従って環境を構築すれば、1つのコマンドで結果族を検証できる——例えば、準リーマン予想の 7/8 の結果など。人類の最良記録は 11/12 であり、7/8 は人類の記録には及ばない前進であり、終点ではない。これは、一般の読者が最先端の AI 数学の主張に対して直接検証を行える最初の機会でもある——証明の詳細を理解する必要はなく、ドキュメントに従ってコマンドを実行するだけでよい。さらに README では、リポジトリ全体をコンパイルするとシステムのメモリマッピング上限に抵触すると特別に警告し、回避用のパラメータを提示している——リポジトリが大きすぎてコンパイル時の落とし穴回避ドキュメントを専用に書く必要があるという事実自体が、1つの注釈となっている。

第二に、CONTENTS.md を検索マップとして使う。 722編もあるため、雑誌のように最初から読み進めるべきではなく、公式がすでに24の分野ごとに結果族をこのファイルにリストアップしているので、まず自分の分野に合わせて興味のある項目を探し、その後で対応する原稿に進むべきだ。通読よりも検索を優先することは、この規模の産出物に向き合う正しいアプローチであり、時間を節約する唯一の方法でもある。

第三に、PDF のみの結論に対しては「未形式化 = 疑わしい」という読書姿勢を保つ。 Lean の証明がない560編の手稿は、検証済みの事実ではなく、証明の主張として読むべきである——これは意地悪な要求ではなく、リポジトリの README 自身が定めた見解である。引用、転述、二次創作の拡散時にこのラベルを付与することは、一般の読者が情報環境のためにできる最も実質的な行動である。

結語

最後は節度を保つ。本号で記録したのは時系列とテキストの照合であり、OpenAIの動機を脳内補完することも、断罪することもしない。同社がアドバイザリーグループの「テスト停止」の要請に対して沈黙を守ったこと、その沈黙自体が記録された事実であり、我々が代わりに語った回答ではない。批判を受けてから今回の公開があったというこの言葉は、タイムラインの要約であり、動機に対する判決ではない。

次の2つの事柄は引き続き注視すべきだ。一つ目は、722件の結果を出力したそのモデルが、ブログで約束された通りに責任を持って公開されるのかどうかである。公開するにせよしないにせよ、それは「どう公開するか」という誠意が原稿の段階で留まるのか、それともモデル自体にまで及ぶのかを直接的に問うことになる。二つ目は、722件のうち、最初に反証または修正される情報がいつ出現するかである。公式側が形式化されておらず誤りがある可能性を自認している前提において、このタイミングが今回の大量放出が最終的にどう評価されるかを大きく左右する。つまり、誠実な示範なのか、それとも検証待ちの主張の山なのかということだ。READMEで約束された「できるだけ早く修正する」に対し、その際どれほど迅速に対応するかも、同様にウォッチリストに載っている。

参考資料

• OpenAI ブログ『Sharing AI progress in mathematics』（2026-10-06、Wayback アーカイブ全文、一次情報）
• github.com/openai/math（一次情報：README、CONTENTS.md、formalization.yaml、comparator ドキュメント；722 原稿 / 372 族 / 132,880 ファイル / 3.1GB / 9832★）
• Hacker News story 49984923（1241▲ / 1412💬、Algolia データ；コメント欄の見解はすべて転述かつ引用符除去、AGMAI 提言および陶哲軒（テレンス・タオ）の投稿はディスカッションエリアからの転引）
• arxiv 2610.08144『Navier–Stokes Lost in Translation』（要旨は一次情報；SCI=∞ 結論の出典）
• 25名のフィールズ賞受賞者による共同声明に関する報道（9-11；本アカウントのトレンド 003 でカバー済み、逆参照）
• Astra 10題、ナビエ-ストークス主張、9月中旬の批判報道（MSN アーカイブ、ForkLog、The Next Web などの二次情報プール、タイムラインアンカー用）