AIの数学における進歩の共有

このリポジトリには、OpenAIの内部モデルによって生成された数学的な論文と、それを裏付ける証明の成果物が含まれています。 モデル開発の一環として、私たちはオープンな研究問題に対してモデルの性能を評価しています。既存の数学的評価での性能が飽和した後、これらの評価を拡張しました。 一部の成果は、以前のモデルによって生成された結果を基にしています。このコレクションには、検証の異なる段階にある結果が含まれています。すべてにLeanによる形式的な証明が伴っているわけではありません。私たちは、それらが得られ次第、このリポジトリにLeanによる形式的な証明を追加し続けていきます。 形式化されていない結果の中には、問題が含まれている可能性があります。私たちは、そのような問題を迅速に修正するよう努めます。また、これらの資料のためのコミュニティホスト型リポジトリも検討しています。 現在のカタログには、372のファミリーに整理された722の論文が含まれています。ファミリーは関連する論文をグループ化しており、主たる結果、補足的な議論、帰結、または代替的な証明が含まれる場合があります。各ファミリーは数学的規律によって分類されます。 ファミリーの説明については、概要から始めてください。個々の論文とそのサポート資料を見つけるには、論文マップを使用してください。 preprints/ ディレクトリには、PDF、ソースファイル、および論文固有の引用とビルド手順が含まれています。Leanライブラリと形式化カタログには、利用可能な形式証明、それに関連する論文、および検証構成が記載されています。追加のチェック手順については、Comparatorの説明を参照してください。 多くの論文（すべてではありません）が形式化されています。 私たちは、以下の結果をカバーする、モデルの推論の簡略化された要約も公開しています。 ファミリー 件名 007 乗法的関数の通常の2点相関 017 πの無理数指数 087 対称的および一般的なマーラー予想 102 基本半正定値閾値における通常のNP硬度 159 等差数列の準多項式境界 197 特性2におけるKaplanskyの直接有限性予想 221 希釈スピンガラスのMézard–Parisi公式 271 量子ハイゼンベルク強磁性体における自発的磁化 287 フリーグループ因子の同型性 362 3次元相対論的Vlasov–Maxwell系 結果の生成方法 結果の大部分は、未公開の内部OpenAIモデルを使用した同じ手順で得られました。平均して、各結果は、そのモデルを使用したChatGPT Proの思考計算で3時間かかりました。 評価の過程で、モデルは約4,000の問題を提示されました。 出力を結果ファミリーと論文に集約し、適切な有意水準を要求した結果、上記のカタログが作成されました。 固定手順からの例外には、リーマンゼータ関数のゼロフリー領域に関する作業と、CMアーベル多様体に対するホッジ予想の証明が含まれます。さらに、リーマンゼータ関数のRe(s) > 11/12ゼロフリー領域の記述は、読みやすさのために人間によって編集されました。 バージョンと引用 このコレクションの公開リリース履歴を維持します。修正と改訂は新しいバージョンとして記録され、以前にリリースされたバージョンは引き続きアクセス可能になります。 個々の論文を引用するには、そのディレクトリにあるBibTeXブロックを使用してください。