素数の間隔は最大186

素数の間隔は最大186

このリポジトリには、Lean 4による素数間隔の上限の形式化と、Pythonによる数値証明が含まれています。Leanでの結果は、3つの明示的な入力公理に条件付けられています。引用されている数学的推定値や数値計算は、まだこれらの入力のLean証明にはなっていません。

結果

素数列 $p_n$ に対して、目標とする上限は

$$\liminf _{n\to\infty}(p _{n+1}-p _n)\le 186.$$

この開発は、以下の入力から $\mathrm{DHL} [40,2]$ を導き出します。すなわち、40個の整数シフトからなる任意の許容集合は、少なくとも2つの素数を含む無限個の平行移動を持ちます。許容性とは、全ての素数 modulo である剰余類を省略することです。これを直径186の含まれるタプルに適用すると、間隔の上限が得られます。

PrimeGaps186.lean の PrimeGap186 名前空間における主な宣言は以下の通りです。

仮定された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.$$

これはDeligneの定理から導かれます。Nicholas M. Katz著『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$ の場合、ランク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』, 2013年6月14日, Proposition 2, p. 1 に記載されています。彼らの正規化された $\mathrm{Kl} _2(c)$ は、和変数 を反転させた後、 $K _2(c;p)/\sqrt p$ に等しくなるため、彼らの $8\sqrt p$ の上限はここでは $8p\sqrt p$ になります。 $A\ne B$ という条件は課されていません。 $A=B$ の場合でも、2つの極は除外されます。

これらの推定値は引用された文献で確立されていますが、このLean開発では未証明の入力として残っています。

数値入力と証明

PrimeGaps186.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 を使用しています。既存のサードパーティ製通知も引き続き適用されます。