OpenAIが10月6日に公開した数学コレクションには、372の結果ファミリーに整理された722件の原稿が含まれます。一つのファミリーに複数の論文が含まれることがあり、形式的証明が対象とする命題は、関連原稿の主張より狭い場合があります。リポジトリで論文から証明設定までたどると、どの主張が検査対象に選ばれたかが分かります。
BIG CHANGEは10月7日、リポジトリの全ファイル一覧、カタログ、選択した証明関連ファイルを調べました。これは文書と静的な成果物の分析です。Leanライブラリのコンパイル、証明チェッカーの実行、数学の査読は行っていません。OpenAIの発表は段階的な公開と説明し、今後さらに形式化を追加するとしています。
大きな変化
- 何が変わったか：研究者は、AIが作成した数百件の原稿を共通の公開カタログで追跡し、関連ファイルまで確認できるようになりました。一部の結果には、形式化された命題や提案された証明実装もあります。
- なぜ重要か：結果の利用を検討する数学者は、実際に検査対象として選ばれた命題、その仮定、論文との関係を確認できます。リポジトリの構成は、より狭い形式的結果がどこまでで、その先にどのような数学的検討が必要かを見分ける助けになります。
- 今後の注目点：OpenAIは形式化を追加し、改訂履歴を保持する予定です。引用したり後続研究の土台にしたりする人にとって、更新は重要です。検討報告には、調べたバージョンと定理を明記する必要があります。
原稿数とファミリー数を分けて数える
今回の一覧では、直下にある原稿ディレクトリを722件確認し、それぞれにPDFが含まれていました。preprints/ の下にはPDFが10件ありました。reasoning_traces/原稿マップには異なる372のファミリー項目と722件の原稿へのリンクがあります。これらは異なる対象を数えています。
成果物
読者が確認できる内容 | 結果ファミリー |
|---|---|
関連する論文のまとまり。補足論証、帰結、別の証明などを含みます。 | 原稿 |
独立した数学文書で、専用のソースファイルと引用情報があります。 | 推論の要約 |
選択した結果について、モデルの推論を短くまとめたものです。 | Lean成果物 |
形式化された定義、命題、提案された証明と、検査対象を特定するリンクや設定です。 | リポジトリの |
READMEは分類を説明し、検証の程度にばらつきがあると注意しています。Leanによる形式化がない結果もあり、OpenAIは形式化されていない研究には問題が含まれる可能性があるとしています。形式化カタログ自体も適用範囲を「部分的な進展」、レビュー状況をと記録しています。これは公開時のメタデータであり、BIG CHANGEの検査結果ではありません。unchecked公開ファイルはOpenAIアカウントなしで読めます。発表では生成モデルを社内モデルとし、公開に向けて作業中だと説明しています。したがって、文書にアクセスできることはモデルへのアクセスを意味しません。
証明を追う前にバージョンを固定する
今回使ったリポジトリのスナップショットはコミット
で、日時は2026年10月6日21:58:50 UTCです。この識別子を含むリンクは調査対象のスナップショットを指し、adc7f1241b42e322a6451854ab7e4b4c146bf78aを含むリンクは変化するデフォルトブランチを指します。OpenAIのREADMEは、訂正や改訂後も以前のリリースを保持するとしています。mainまず
概要で数学分野別のファミリーを確認し、原稿マップで対象論文を探します。ディレクトリ名、リポジトリのコミット、論文に付属する引用情報を記録してください。原稿の日付とコレクションの公開日は異なることがあります。ファミリー003には、7/8より右側に零点のない領域があると主張する論文、11/12より右側の領域に関する別証明、Landau–Siegel零点を扱う別の論文があります。
最初の論文のディレクトリの日付は9月30日で、BibTeX形式の引用が付いています。対象の論文を記録すれば主張を区別できます。その
Leanの適用範囲ページには形式化が扱う命題、対象外の項目、論文中の後続の応用が省略されていることが記載されています。ゼータ関数の結果、DirichletとHeckeのL関数、一様な実零点間隔について、別々の検査命題にリンクしています。一つの命題の検査がページ内の全項目を表すわけではありません。選択された命題を設定までたどる
OpenAIの
Comparatorの説明書はファミリー003を例にしています。Comparatorは提案されたLean証明を指定された課題と比較するツールです。例のJSON設定は一つの定理を選びます。引数の実部が7/8を超えるとき、リーマンゼータ関数がゼロにならないという命題です。設定は課題モジュールと別の解答モジュールを指定します。標準公理
、propext、Quot.soundを許可し、Classical.choiceをenable_nanodaに設定します。NanodaはComparatorが利用できる独立チェッカーですが、この設定例では有効になっていません。false課題ファイル
にはがあります。これは未完成の証明を示すLeanのプレースホルダーです。ここでは照合対象の命題を提示します。Comparatorの文書は課題内のプレースホルダーを許可し、解答には正しい証明を求めます。この課題だけでを見つけても、別の解答が通るかは分かりません。sorryComparatorの説明書sorry。Comparatorの説明書。
文書化されたローカル検査では、この設定、challengeモジュールとsolutionモジュール、および依存関係を入力として使います。リポジトリが固定しているのはLean 4.34.1です。そのLakeマニフェストにはMathlibを含む依存関係のリビジョンが記録されています。Mathlibのリビジョンはd13f23b723b8a846827a245b89c10fc7d3f11612です。
OpenAIはcomparator, landrunとlean4exportを実行ファイルの検索パスに含めるよう求め、その後、次のコマンドをlean/ディレクトリから実行するよう説明しています。
lake update
lake exe cache get
lake env comparator ComparatorChallenges/QuasiRiemannHypothesis.jsonこれらは公開者の手順であり、私たちが実行したコマンドではありません。3つの外部ツールのバージョンは固定されていません。Comparatorの現行文書は互換性のあるlean4exportを求め、サンドボックスの前提条件と、challengeとの一致、許可された公理の使用、カーネルによる受理を成功の条件とする方法を説明します。再現可能な報告には、リポジトリのコミットに加え、インストール済みツールのバージョンと実際の出力を記録する必要があります。
このLeanライブラリのREADMEは、大規模なライブラリの一部を選んでコンパイルすることを勧めています。また、Linuxのメモリマッピング制限によって全体をビルドできない場合があると説明しています。この例のローカル実行時間やハードウェア費用は測定していません。
成功した検査は、明示された範囲で読む
Leanの検証リファレンスは、形式的証明の受理と定理の意味の解釈を区別しています。参照した文書はバージョン4.35.0-rc3で、リポジトリが固定するツールチェーンとは別です。
基本検査の成功は、定義、インポート、公理のもとでカーネルが形式的命題を受理したことを意味します。依存関係には未完成の証明が残る場合があります。Leanは使用された公理を表示するために#print axiomsを使い、依存関係内の未完成の証明にはsorryAxが含まれます。
より強い検査では保存済みの証明を再実行したり、解答を別途指定された命題と比較したりします。それでも検査環境と、意図した意味が正確に表現されているかに依存します。検証報告には、正確なchallenge、許可された公理、外部チェッカーの設定を記録する必要があります。カーネルによる受理もchallengeとの一致も、学術誌の採択や原稿のすべての主張が形式化されたことを示すものではありません。
計算量の数値は生成についてのもの
OpenAIは、平均的な結果ごとにChatGPT Proで約3時間考えるのに相当する計算量を使ったと報告しています。READMEによると、評価では約4,000問を提示し、出力をグループ化して重要と判断した結果を選びました。通常の手順からの例外も記載しています。これらは企業側の生成時の数値であり、読者がLeanで検査する費用や総額のドル請求を示すものではありません。公開発表, 生成についての説明。
ファミリー003について、今回の調査では特定のゼータ関数の命題、提案された解答、チェッカーが許可する公理を確認しました。提供された例ではNanodaが無効になっていることも確認しています。この設定で検査が成功するかどうかは、実際に実行して記録する必要があります。
出典・参考資料
- OpenAIの10月6日の発表は公開日、モデルの社内での位置づけ、予定される追加、同社の計算量推定を裏づけます。これは開発者自身による説明です。
- 固定されたリポジトリには、ここで調べたカタログ、原稿ファイル、証明設定があります。件数は完全なファイル一覧と原稿マップに基づきます。選んだ形式ファイルは実行せずに読み、概要の構成を知るためLaTeXソースも確認しました。
- Leanの検証リファレンスは証明検査の意味と限界を説明します。参照文書は4.35.0-rc3で、OpenAIのプロジェクトはLean 4.34.1を固定しています。
- Comparatorの説明書はchallengeとsolutionのファイル、環境要件、条件付きの保証を説明します。このコレクションの検証結果は報告していません。
- Curtis PykeによるKingy.aiのレビューは公開内容を独立して静的に調査しています。Leanを独立実行していないと明記しているため、証明検査の再現とは扱いません。
- BIG CHANGEの以前のAI数学記事は5月から9月までの流れを扱っています。この記事では、新しいコレクションの成果物構成と調査手順を検討します。
