素数の間隔は最大186

素数の間隔は最大186 このリポジトリには、素数の間隔の上限に関するLean 4による形式化と、Pythonによる数値証明が含まれています。Leanによる結果は、3つの明示的な入力公理に条件付きです。引用されている数学的推定値や数値計算は、これらの入力のLean証明にはまだ変換されていません。 結果 素数列 $p_n$ に対して、目標とする上限は $$ ím inf_{n\to\infty}(p_{n+1}-p_n)\le 186 $$ です。この開発は、以下の入力から $\mathrm{DHL}[40,2]$ を導き出します。すなわち、40個の整数のシフトからなる任意の許容集合は、少なくとも2つの素数を含む無限個の平行移動を持ちます。許容性とは、全ての素数に関する剰余類を1つずつ除外することを意味します。これを直径186の含まれるタプルに適用すると、間隔の上限が得られます。 PrimeGaps186.lean の主な宣言（名前空間 PrimeGap186）は以下の通りです。 宣言 Result $\mathrm{DHL}[40,2]$ を全ての許容整数のタプルに対して。 infinite_two_prime_translates_admissibleTuple 明示的なタプルの2つの素数を持つ平行移動が無限に存在すること。 primeGapLiminf_le_186 連続する素数の間隔の上限。 仮定されたDeligne型推定値 素数 $p$ に対して、$e_p(x)=\exp(2\pi i\widetilde{x}/p)$ と書きます。ここで $\widetilde{x}$ は $x\in\mathbb{F}_p$ の任意の整数代表値です。 $$ \mathrm{Kl}_3(c;p) =\frac1p\sum_{\substack{x_1,x_2,x_3\in\mathbb{F}_p\\x_1x_2x_3=c}} e_p(x_1+x_2+x_3), $$ $$K_2(c;p)=\sum_{u\in\mathbb{F}_p^\times}e_p(u+c/u). $$と定義します。 公理 PrimeGap186.kloosterman3_bound は、全ての素数 $p$ と全ての $c\in\mathbb{F}_p^\times$ に対して以下のバウンドを仮定します。 $$ \left|\mathrm{Kl}_3(c;p)\right|\le 3. $$これは Nicholas M. Katz による Deligne の定理から導かれます（Gauss Sums, Kloosterman Sums, and Monodromy Groups, Annals of Mathematics Studies 116, Princeton University Press (1988), Theorem 4.1.1(1)–(2), p. 49）。$n=3$、$b_1=b_2=b_3=1$、$n=3$、$b_1=b_2=b_3=1$、自明な乗法的文字、ランク3、重み2の場合、生のバウンドは $3p$ となります。我々の正規化では $p$ で割っています。 公理 PrimeGap186.kloosterman2_correlation_bound は、全ての素数 $p$ と全ての $A,B\in\mathbb{F}_p^\times$ に対して以下のバウンドを仮定します。 $$ \left|\sum_{t\in\mathbb{F}_p\setminus\{0,-1\}} K_2(A/t;p)\,K_2(B/(t+1);p)\right|\le 8p\sqrt p. $$これは Étienne Fouvry, Emmanuel Kowalski, Philippe Michel による The Friedlander–Iwaniec character sum (14 June 2013, Proposition 2, p. 1) に基づいています。彼らの正規化された $\mathrm{Kl}_2(c)$ は、和変数を反転させた後、ここで $8p\sqrt p$ となる $8\sqrt p$ のバウンドに相当します。 $A\ne B$ という条件は課されていません。2つの極は $A=B$ の場合でも除外されています。これらの推定値は引用された文献で確立されていますが、このLean開発では未証明の入力として残っています。 数値入力と証明 PrimeGap186.physical_integral_bounds は、104個の外部および45個の内部物理積分上限、さらに3つのキャップ上限を仮定します。Python証明書は、トライアルをゼロから再計算します。 テストされた環境は、Python 3.12.13、NumPy 2.2.6、python-flint 0.9.0、および修正された符号付き多項式畳み込み（バンドルされていない）を備えたカスタムFLINT 3.6.0ビルドを使用しました。 python3 -B prime_gap_186_certificate.py --workers 4 --output prime_gap_186_fresh.json 新しい出力パスを使用してください。PYTHONOPTIMIZE を未設定のままにし、-O または -OO を使用しないでください。必須の浮動小数点および符号付き畳み込みチェックに合格する必要があります。成功した実行は、passed: true を示すレシートを生成しますが、Lean公理を放電するものではありません。 ビルドと検証 プロジェクトは Lean 4.34.0-rc2 とそのMathlib依存関係をピン留めしています。elan がインストールされている場合、以下を実行します。 lake exe cache get lake build PrimeGaps186 登録されたLeanビルドは、エラーや警告なしでパスしました。Comparatorは3つの結果すべてをChallenge.leanと一致させ、NanodaとLeanのカーネルはローカルのColima Linux VMでそれらの証明を受け入れました。この構成は、文書化された3つのプロジェクト公理に加えて、propext、Quot.sound、Classical.choice（合計6つ）を許可します。これにより、入力自体ではなく、条件付き証明が検証されます。数値証明書は、以前の正常な実行から変更されていません。Challenge.lean は、ステートメントと入力仮定を指定しており、3つの意図的な定理プレースホルダーがあります。チェック設定とステータスについては、Comparatorの指示と形式化メタデータを参照してください。プロジェクトへの貢献はApache 2.0ライセンスであり、既存のサードパーティ製通知が引き続き適用されます。