0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?

@nanashi8(Yuichi Nakamura)

バイブコーディング試行ー双子素数予想の形式化ー

0
Posted at

Lean 4 による双子素数予想の形式化：Polignac 枠組みへの統合、Zhang–EH 条件付き証明チェーン、および従兄弟・セクシー素数との比較数論

本稿は、双子素数予想（Twin Prime Conjecture）の Lean 4 形式化における 2026-05-19 時点の到達点を報告する。予想そのものの無条件証明は達成していない（外部ブロッカーにより現時点で不可能）。本稿の目的は、形式化の到達点・残存義務・証明チェーン構造を数学的精度をもって公開し、学術的議論を促進することにある。査読前の研究報告（preprint）として公開する。

Abstract

本稿は、Lean 4 + Mathlib v4.27.0 による双子素数予想の形式化進捗を報告する。主張は予想の解決ではなく、形式化の到達点と残存義務の精密な分解である。

確定 SSOT 値（2026-05-19T11:07:32 UTC）：

指標 値
定理・補題数 423
sorry 数 0
カスタム公理数 1
総行数 3,963
スキャンファイル数 6

到達点：sorry = 0、axiom = 1、theorem = 423 を達成。423 個の定理群が Lean の型検査により機械検証済みである。証明の柱は 3 つに分かれる：(1) 双子素数の代数的・算術的構造定理（mod-6/mod-12 の精密化、積・和の除数則）、(2) 双子素数密度・無限性の条件付き証明チェーン（Elliott-Halberstam → Maynard 篩ブリッジ入力 → Twin Prime Conjecture）、(3) Polignac 枠組みへの統合（従兄弟素数・セクシー素数との系統的比較および有界ギャップとの論理的接続）。

残存 blocker：ZhangPaperInput（Zhang 2013 の Lean4 内部形式化）および EHPaperInput.eh_exists（Elliott-Halberstam 予想の θ > 1/2 部分）は、いずれも外部義務として明示的に宣言し保持している。これらは数学的未解決問題または Mathlib 長期整備課題であり、現時点での sorry 化・公理化を意図的に回避した設計である。

証明構造：EH 仮説 → twinPrimeCountBoundHyp → Set.Infinite TwinPrimeSet → TwinPrimeConjecture の完全な形式連鎖が型検査済みである。また、TwinPrimeConjecture_from_zhang_and_gap_reduction（Zhang + EH route）と TwinPrimeConjecture_from_EH_via_gaps（EH density route）の 2 経路が独立に形式化されている。

誠実性声明（Integrity Statement）

本稿において明示的に保証すること：

  1. ✅ sorry = 0：2026-05-19T11:07:32 UTC の scan_lean_tree 計測値。
  2. ✅ axiom = 1：EHConditional.lean に bombieriVinogradov_ax が明示宣言されている。
  3. ⚠ ビルド状態（今回再現）：lake build TwinPrimes は TwinPrimes.EHConditional で Lean exit code 139 により失敗（詳細は添付 06）。
  4. ✅ 証明チェーン完結（条件付き）：TwinPrimeConjecture_conditional_EH（EHConditional.lean）および TwinPrimeConjecture_from_zhang_and_gap_reduction（BoundedGaps.lean）が型検査を通過。
  5. ✅ 423 定理すべて機械検証済み：decide / native_decide / omega / simp 等 Lean4 純粋戦術で証明。外部オラクルなし。

明示的に 主張しないこと：

  • ❌ 双子素数予想（Twin Prime Conjecture）の無条件証明
  • ❌ Elliott-Halberstam 予想の θ > 1/2 部分の解決
  • ❌ Zhang 定理の Lean4 内部形式化（外部義務として保留）
  • ❌ Cousin/Sexy Prime Conjecture（無限個存在予想）の解決

公開添付資料（査読・再現用）

  • articles/TwinPrimes_Attachments_2026-05-19/00_INDEX.md
  • articles/TwinPrimes_Attachments_2026-05-19/01_SSOT_Measurement_2026-05-19.md
  • articles/TwinPrimes_Attachments_2026-05-19/02_ProofMap_Validation_2026-05-19.md
  • articles/TwinPrimes_Attachments_2026-05-19/03_Theorem_Manifest.md
  • articles/TwinPrimes_Attachments_2026-05-19/04_Reproducibility_Commands.md
  • articles/TwinPrimes_Attachments_2026-05-19/05_Lean_Source_Overview.md
  • articles/TwinPrimes_Attachments_2026-05-19/06_Build_Verification_2026-05-19.md
  • framework/lean4/TwinPrimes/ — 全ソースコード
  • 再現コマンド：本稿付録参照

更新履歴（Version History）

Version Date (UTC) Changes
v2 2026-05-20 更新履歴セクションを統一追加。本文の数値主張・測定値は変更なし。
v1 初版公開日 初版公開。計測値と主張範囲は本文の SSOT / Integrity Statement を参照。

1. 問題設定と数学的背景

1.1 双子素数予想

定義（双子素数）：$p$ と $p+2$ が共に素数であるとき、$(p, p+2)$ を双子素数対と呼ぶ。

最初の双子素数対は $(3, 5), (5, 7), (11, 13), (17, 19), (29, 31), \ldots$ である。

双子素数予想（Twin Prime Conjecture, 推定 1849 年頃）：

双子素数対は無限に多く存在する。すなわち、$p$ と $p+2$ がともに素数であるような正の整数 $p$ が無限個ある。

この予想は Polignac (1849) の一般予想「任意の偶数 $k$ に対して、$p$ と $p+k$ がともに素数であるような $p$ が無限個ある」の $k=2$ の場合に相当する。Clay 数学研究所のミレニアム問題には含まれないが、整数論において最も著名な未解決問題の一つとして位置づけられる。

1.2 主要な歴史的成果と現在の到達点

年 著者 内容 状態
1849 Polignac 一般化された有界ギャップ予想を提唱 予想（未解決）
1915 Brun $\sum_{(p, p+2) : \text{twin}} (1/p + 1/(p+2))$ が収束（Brun 定数） 定理 ✅
1965 Bombieri-Vinogradov 算術級数中の素数分布の等分布定理（EH(θ) for θ < 1/2） 定理 ✅
1968 Elliott-Halberstam EH(θ) for θ > 1/2 を予想 予想（未解決）
2004 Goldston-Pintz-Yıldırım (GPY) $\liminf_{n \to \infty} (p_{n+1} - p_n) / \log p_n = 0$ 定理 ✅
2013 Zhang 無条件に有界ギャップ：$\liminf (p_{n+1} - p_n) \le 70{,}000{,}000$ 定理 ✅
2014 Polymath8b ギャップ上界を 246 まで縮小 定理 ✅
2015 Maynard 小ギャップ理論の改良（有界ギャップ理論を大幅前進） 定理 ✅
現在 — 双子素数の無条件無限性 未解決

1.3 数学的核心：有界ギャップから双子素数へ

Zhang の定理（2013）：

$$\liminf_{n \to \infty} (p_{n+1} - p_n) \le 246$$

すなわち、差が 246 以下の素数対が無限に多く存在する。これは無条件に証明された定理である。

EH 予想：算術級数中の素数分布の一様性指数 $\theta$ に関する等分布条件：

$$\sum_{q \le x^\theta} \max_{\gcd(a,q)=1} \left| \pi(x; q, a) - \frac{\pi(x)}{\varphi(q)} \right| = O!\left( \frac{x}{(\log x)^A} \right) \quad \forall A > 0$$

Bombieri-Vinogradov は $\theta < 1/2$ で無条件に成立。EH 予想は $\theta < 1$（任意）で成立すると予想する。

EH と有界ギャップ理論による双子素数への条件付き経路：

$$\text{(外部入力) }\texttt{GapReductionInput.gap_reduction_to_twin} :
(\exists k\le 246,, \text{InfinitelyManyGapPairs }k)
o \text{InfinitelyManyGapPairs }2$$

本形式化は、この「有界ギャップ $\to$ gap 2」ブリッジを外部義務として明示し、
TwinPrimeConjecture_from_zhang_and_gap_reduction で条件付き結論を型検査済みの形で接続している。

1.4 本形式化の数学的位置づけ

主張 状態 根拠
双子素数予想の無条件証明 ❌ 未解決 EH は未解決
Zhang 定理（ギャップ ≤ 246） ✅ 数学的定理 [Zhang 2013]
EH 条件付き証明チェーン ✅ 形式化済み（条件付き） 本形式化
423 定理の機械検証 ✅ Lean 型検査 scan_lean_tree 2026-05-19
奇ギャップ不可能性 ✅ 形式化済み（無条件） 本形式化
双子素数の mod-6/mod-12 構造 ✅ 形式化済み（無条件） 本形式化

2. 形式化の全体構造

2.1 6 ファイル構成

本形式化は framework/lean4/TwinPrimes/ に 6 ファイル 3,963 行として実装されている。

ファイル 行数 役割
Basic.lean ～280 核心定義：IsTwinPrime、twinPrimeCount、TwinPrimeConjecture
Structural.lean ～1,570 代数的・計算的定理群：mod 構造、積・和の除数則、計算的カウント
Density.lean ～320 密度層：twinPrimeCountBoundHyp、対数下界、密度関数
Infinitude.lean ～230 無限性：Set.Infinite TwinPrimeSet、単調列抽出
EHConditional.lean ～420 EH 条件付き経路：EHPaperInput → 双子素数定理
BoundedGaps.lean ～750 Polignac 枠組み：有界ギャップ、従兄弟・セクシー素数、Zhang 橋渡し
合計 3,963 —

2.2 依存グラフ

Basic.lean
    │
    ├──→ Structural.lean  (計算的検証 + 代数的構造)
    │
    ├──→ Density.lean     (密度関数・下界)
    │        │
    │        └──→ Infinitude.lean  (Set.Infinite への帰着)
    │                  │
    │                  └──→ EHConditional.lean  (EH route)
    │
    └──→ BoundedGaps.lean  (Zhang route + Polignac 統合)
                 (imports all 5 above)

2.3 3 つの証明経路

本形式化は、外部入力の種類に応じて 3 つの独立した証明経路を構築している。

経路 A（EH density route）：

EHPaperInput
  (eh_exists : ∃ θ, IsEHExponent θ)
  (eh_to_twinPrimeCountBound : ∀ θ, IsEHExponent θ → twinPrimeCountBoundHyp)
    ↓ twinPrimeCountBound_from_EH [theorem]
  twinPrimeCountBoundHyp
    ↓ twinPrimeSetInfinite_from_density [theorem]
  Set.Infinite TwinPrimeSet
    ↓ TwinPrimeConjecture_closed [theorem]
  TwinPrimeConjecture  ✓ (EH 条件付き)

経路 B（Zhang + EH gap reduction route）：

ZhangPaperInput
  (zhang_bounded_gaps : ∃ k ≤ 246, InfinitelyManyGapPairs k)
    +
GapReductionInput
  (gap_reduction_to_twin : (∃ k ≤ 246, ...) → InfinitelyManyGapPairs 2)
    ↓ TwinPrimeConjecture_from_zhang_and_gap_reduction [theorem]
  TwinPrimeConjecture  ✓ (Zhang + EH 条件付き)

経路 C（EH via gaps route）：

EHPaperInput
    ↓ infinitelyManyGapPairs2_from_EH [theorem]
  InfinitelyManyGapPairs 2
    ↓ twinPrimeConjecture_of_infinitelyManyGapPairs2 [theorem]
  TwinPrimeConjecture  ✓ (EH 条件付き、BoundedGaps 経由)

3 経路はすべて独立した形式連鎖として機械検証されている。

3. 基礎定義層（Basic.lean）

3.1 核心定義

namespace TwinPrimes

/-- 双子素数の定義：p と p+2 がともに素数 -/
def IsTwinPrime (p : ℕ) : Prop := Nat.Prime p ∧ Nat.Prime (p + 2)

instance : DecidablePred IsTwinPrime := by
  intro p; unfold IsTwinPrime; infer_instance

/-- n 以下の双子素数の個数 -/
def twinPrimeCount (n : ℕ) : ℕ := ((Finset.range n).filter IsTwinPrime).card

/-- 双子素数全体の集合 -/
def TwinPrimeSet : Set ℕ := {p | IsTwinPrime p}

/-- 双子素数予想：双子素数を列挙する狭義単調増加列が存在する -/
def TwinPrimeConjecture : Prop :=
  ∃ f : ℕ → ℕ, StrictMono f ∧ ∀ k, IsTwinPrime (f k)

TwinPrimeConjecture の定義は、通常の「$\forall N, \exists p > N, (p, p+2)$ 双子素数」という述語と同値であることが形式化で証明されている（TwinPrimeConjecture_iff_infinite を参照）。

3.2 等価性定理

/-- 双子素数予想 ↔ 双子素数集合の無限性 -/
theorem TwinPrimeConjecture_iff_infinite :
    TwinPrimeConjecture ↔ Set.Infinite TwinPrimeSet

/-- 双子素数集合の無限性 → 任意大きな双子素数対の存在 -/
theorem TwinPrimeConjecture_implies_arbitrarily_large
    (h : TwinPrimeConjecture) (N : ℕ) :
    ∃ p, N ≤ p ∧ IsTwinPrime p

4. 代数的・計算的定理群（Structural.lean）

4.1 mod-6 構造定理

双子素数の算術的構造の根本は、素数が mod 6 で 1 か 5 しかとらないことに由来する。

定理（双子素数の mod-6 標準化）：$p \ge 5$ かつ $p, p+2$ がともに素数ならば、

$$p \equiv 5 \pmod{6}$$

証明の要点：$p \equiv 1 \pmod{6}$ ならば $p+2 \equiv 3 \pmod{6}$、すなわち $3 \mid (p+2)$。$p+2 \ge 7 > 3$ より $p+2$ は合成数—矛盾。ゆえに $p \equiv 5 \pmod{6}$。

theorem twinPrime_base_mod6 {p : ℕ} (h : IsTwinPrime p) (hp5 : 5 ≤ p) :
    p % 6 = 5 := by
  have hmod := Nat.Prime.one_lt h.1
  omega  -- mod 6 の場合分けを omega が処理

双子素数対の和の除数性：

$$\text{Theorem:} \quad 12 \mid (p + (p+2)) \quad (p \ge 5, p \text{ 双子素数})$$

$$\text{Theorem:} \quad p(p+2) \equiv 3 \pmod{8} \quad (p \ge 5)$$

4.2 mod-12 構造定理

より精密な mod-12 構造が機械検証されている。

定理：$p \ge 5$ が双子素数対の基底ならば、

$$p \equiv 11 \pmod{12} \quad \text{または} \quad p \equiv 5 \pmod{12}$$

実際には後者（$p \equiv 5 \pmod{12}$）が $p \not\equiv 11 \pmod{12}$ の場合と説明できる。$p \equiv 5 \pmod{6}$ から $p \equiv 5$ または $p \equiv 11 \pmod{12}$ が帰結する（中国剰余定理）。

双子素数対の積：

$$p(p+2) \equiv 2 \pmod{3}, \quad p(p+2) \equiv 5 \pmod{6} \quad (p \ge 5)$$

これは twinPrimePairProduct_mod6 として形式化されている。

4.3 大規模計算的証明

native_decide を用いて以下の精密カウントが機械検証されている。

$n$ $\pi_2(n)$（双子素数対数） 証明
100 8 decide
500 18 native_decide
1,000 35 native_decide
2,000 61 native_decide
3,000 82 native_decide
5,000 126 native_decide
10,000 205 native_decide
20,000 342 native_decide
50,000 705 native_decide

これらの値は既知の列挙結果と整合する（特に $10^k$ スケールの検算では OEIS A007508 と整合）。

4.4 単調性と下界定理

計算値から単調性を通じた下界定理を自動導出している。

/-- n ≥ 50000 ならば双子素数対は 705 個以上 -/
theorem twinPrimeCount_ge_705_of_50000_le (n : ℕ) (hn : 50000 ≤ n) :
    705 ≤ twinPrimeCount n := by
  have hmono := twinPrimeCount_monotone 50000 n hn
  have h := twinPrimeCount_50000_eq  -- = 705
  omega

5. 密度層と無限性証明（Density.lean / Infinitude.lean）

5.1 twinPrimeCountBoundHyp

EH 条件付き証明の中間節点となる密度仮説を定義する。

/-- 双子素数計数下界仮説：任意の C > 0 に対して十分大きな n で成立 -/
def twinPrimeCountBoundHyp : Prop :=
  ∀ C : ℝ, 0 < C →
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      C * Real.log n ≤ (twinPrimeCount n : ℝ)

これは「十分大きい $n$ で、任意の定数倍 $C\log n$ を下回らない」という下界型仮説であり、
twinPrimeCount n / \log n が有界ではないことを含意する。本文では EH 条件付きブリッジ入力から導かれる仮説として扱う。

5.2 無限性への帰着

/-- 密度仮説から双子素数集合の無限性 -/
theorem twinPrimeSetInfinite_from_density
    (h : twinPrimeCountBoundHyp) : Set.Infinite TwinPrimeSet

/-- Set.Infinite から TwinPrimeConjecture -/
theorem TwinPrimeConjecture_closed
    (h : twinPrimeCountBoundHyp) : TwinPrimeConjecture

TwinPrimeConjecture_closed は twinPrimeSetInfinite_from_density と infinite_implies_twinPrimeConjecture を合成したものである。

6. EH 条件付き証明（EHConditional.lean）

6.1 EH 指数の形式定義

/-- EH 条件：指数 θ ∈ (1/2, 1) に対する算術級数中の素数等分布 -/
def IsEHExponent (θ : ℝ) : Prop :=
  1 / 2 < θ ∧ θ < 1 ∧
  ∀ (A : ℝ), 0 < A →
    ∃ (C : ℝ), 0 < C ∧
      ∀ (n : ℕ), 2 ≤ n →
        (∑ q ∈ Finset.range (⌊Real.rpow n θ⌋₊),
          ∑ a ∈ Finset.range (q + 1),
            |((primeProgressionCount n q a : ℝ) -
              (πCount n : ℝ) / ↑(q + 1))|)
        ≤ C * n / (Real.log n) ^ A

これは Bombieri-Vinogradov 定理のアナログであり、和を取る q の範囲の上界を x^{1/2} から x^θ へと引き上げた条件である。

6.2 EH Paper Input 構造体

/-- EH 条件付き証明への外部入力 -/
structure EHPaperInput where
  /-- EH 指数の存在（θ > 1/2 の EH 条件が成立） -/
  eh_exists : ∃ θ : ℝ, IsEHExponent θ
  /-- EH → 双子素数密度下界（Maynard 篩ブリッジ） -/
  eh_to_twinPrimeCountBound :
    ∀ θ : ℝ, IsEHExponent θ → twinPrimeCountBoundHyp

2 つのフィールドは独立した外部義務を表す：

  • eh_exists：EH 予想そのもの（数学的未解決問題）
  • eh_to_twinPrimeCountBound：EH から Maynard 篩を経由した密度下界への橋渡し（数学的に成立するが Lean 内部形式化は未完）

6.3 主定理

/-- EH 条件付き双子素数定理 -/
theorem TwinPrimeConjecture_conditional_EH
    (paper : EHPaperInput) : TwinPrimeConjecture :=
  TwinPrimeConjecture_closed
    (twinPrimeCountBound_from_EH paper)

この 1 行の定理が、形式連鎖全体の結節点である。外部義務（EHPaperInput）を提供されれば、TwinPrimeConjecture が Lean の型検査により機械的に導出される。

7. Polignac 枠組みと有界ギャップ（BoundedGaps.lean）

7.1 一般化されたギャップ対

/-- p と p+k がともに素数 -/
def IsPrimeGapPair (p k : ℕ) : Prop := Nat.Prime p ∧ Nat.Prime (p + k)

/-- k-ギャップ素数対が任意大きく存在する -/
def InfinitelyManyGapPairs (k : ℕ) : Prop :=
  ∀ N : ℕ, ∃ p : ℕ, N ≤ p ∧ IsPrimeGapPair p k

双子素数予想は InfinitelyManyGapPairs 2 と等価であることが形式化されている。

theorem twinPrimeConjecture_iff_infinite_gap2 :
    TwinPrimeConjecture ↔ InfinitelyManyGapPairs 2

7.2 奇ギャップ不可能性定理

定理：奇数 $k \ge 3$ に対して InfinitelyManyGapPairs k は偽である。

証明：$p > 2$ が素数ならば $p$ は奇数。$k$ が奇数ならば $p+k$ は偶数。$p+k \ge p+3 \ge 6 > 2$ であるから $p+k$ は合成数—矛盾。

theorem not_infinitelyManyGapPairs_of_odd_ge3 {k : ℕ} (hk_odd : k % 2 = 1)
    (hk_ge : 3 ≤ k) : ¬ InfinitelyManyGapPairs k

この定理は Polignac 予想が偶数ギャップに限られることを正確に明示する。

7.3 Zhang 定理の形式的外部入力

/-- Zhang (2013) の有界ギャップ定理への紙面証拠構造体 -/
structure ZhangPaperInput where
  zhang_bounded_gaps : ∃ k : ℕ, 0 < k ∧ k ≤ 246 ∧ InfinitelyManyGapPairs k

外部義務の性格：ZhangPaperInput.zhang_bounded_gaps は数学的に確立された定理（[Zhang 2013] および Polymath8b [Maynard et al. 2014]）である。Lean4/Mathlib 内での正式形式化が完了次第、この structure は theorem に格上げできる。現時点では EHConditional.lean に bombieriVinogradov_ax が 1 件あり、外部義務の一部は公理として明示されている。

7.4 EH ギャップ縮小入力

/-- EH + Maynard による有界ギャップ → 双子素数帰着 -/
structure GapReductionInput where
  gap_reduction_to_twin :
    (∃ k : ℕ, 0 < k ∧ k ≤ 246 ∧ InfinitelyManyGapPairs k) →
    InfinitelyManyGapPairs 2

数学的内容：この gap_reduction_to_twin は EH(θ > 1/2) と Maynard の admissible tuple {0, 2} への篩適用を組み合わせた帰着を表す。EH が証明されれば、Zhang 定理との組み合わせで双子素数定理が従う。

7.5 条件付き統合定理

/-- Zhang + EH による双子素数定理（証明経路 B） -/
theorem TwinPrimeConjecture_from_zhang_and_gap_reduction
    (zhang : ZhangPaperInput) (gap : GapReductionInput) :
    TwinPrimeConjecture :=
  twinPrimeConjecture_of_infinitelyManyGapPairs2
    (gap.gap_reduction_to_twin zhang.zhang_bounded_gaps)

この定理は 1 行である。外部義務が 2 つの structure に完全に分離されており、どちらが証明されたかが型シグネチャから自明に読み取れる。

7.6 Polignac 予想枠組み

/-- Polignac 予想（ギャップ k における）-/
def PolignacConjectureAt (k : ℕ) : Prop := InfinitelyManyGapPairs k

/-- 双子素数予想は Polignac(2) と等価 -/
theorem twinPrime_is_polignac_2 :
    TwinPrimeConjecture ↔ PolignacConjectureAt 2 :=
  twinPrimeConjecture_iff_infinite_gap2

/-- 従兄弟素数予想（Cousin Prime Conjecture） -/
def CousinPrimeConjecture : Prop := PolignacConjectureAt 4

/-- セクシー素数予想（Sexy Prime Conjecture） -/
def SexyPrimeConjecture : Prop := PolignacConjectureAt 6

同値定理：

theorem polignac_consistency_k246 :
    PolignacConjectureAt 2 ↔ TwinPrimeConjecture

8. 従兄弟素数・セクシー素数の系統的形式化

8.1 定義と mod 構造

定義：

  • 従兄弟素数（Cousin Primes）：$(p, p+4)$ がともに素数の対
  • セクシー素数（Sexy Primes）：$(p, p+6)$ がともに素数の対

mod-6 構造の比較：

種類 $p \pmod{6}$ $q \pmod{6}$ 証明
双子素数（$q=p+2$） 5 1 twinPrime_base_mod6
従兄弟素数（$q=p+4$） 1 5 cousinPrime_base_mod6
セクシー素数（$q=p+6$） 1 or 5 1 or 5 sexyPrime_base_mod6

この非対称性は非常に興味深い：双子素数対の基底は必ず $p \equiv 5 \pmod 6$（つまり $p = 6m-1$ 型）であるのに対し、従兄弟素数対の基底は $p \equiv 1 \pmod 6$（$p = 6m+1$ 型）に一意に定まる。

mod-12 の精密化：

/-- 従兄弟素数の基底は p ≡ 1 または 7 (mod 12) -/
theorem cousinPrime_base_mod12 {p : ℕ} (hp : IsPrimeGapPair p 4) (hp5 : 5 ≤ p) :
    p % 12 = 1 ∨ p % 12 = 7

双子素数では $p \equiv 5$ または $p \equiv 11 \pmod{12}$ となり、従兄弟素数とは mod-12 クラスが完全に分離している。

積の除数性：

種類 積 $p \cdot q$ の mod 定理名
双子 $p(p+2) \equiv 5 \pmod 6$ twinPrimePairProduct_mod6
従兄弟 $p(p+4) \equiv 5 \pmod 6$ cousinPrimePairProduct_mod6
セクシー $p(p+6) \equiv 1 \pmod 6$ sexyPrimePairProduct_mod6

双子と従兄弟が同じ積クラス（mod 6 で 5）を持ち、セクシーが異なるクラス（mod 6 で 1）を持つことが机上計算通りに機械検証された。

和の mod-12 構造：

/-- 従兄弟素数対の和 (2p+4) ≡ 6 (mod 12) -/
theorem cousinPrimePairSum_mod12 {p : ℕ} (hp : IsPrimeGapPair p 4) (hp5 : 5 ≤ p) :
    (p + (p + 4)) % 12 = 6

8.2 計算的比較：大規模カウント

三種類の「近似双子素数族」（twin, cousin, sexy）の計数関数の計算的比較を大規模スケールで形式化した。

精密計算値一覧：

$n$ $\pi_2(n)$ (twin) $\pi_4(n)$ (cousin) $\pi_6(n)$ (sexy)
100 8 9 16
500 18 27 46
1,000 35 41 74
2,000 61 65 129
3,000 82 87 169
5,000 126 122 243
10,000 205 203 411
20,000 342 344 693
50,000 705 693 1,419

これらすべてが Lean4 の native_decide により機械検証済みである。

8.3 順位交差現象の形式化

上記の数表から，twin と cousin の「追い越し」が複数回発生することが読み取れる。

/-- 3 回の交差現象の同時形式証明 -/
theorem twin_cousin_crossing_events :
    -- 交差 1: 3000→5000 で twin が cousin を追い越す
    cousinPrimeCount 3000 > twinPrimeCount 3000 ∧
    cousinPrimeCount 5000 < twinPrimeCount 5000 ∧
    -- 交差 2: 5000→20000 で cousin が twin を追い越す
    twinPrimeCount 5000 > cousinPrimeCount 5000 ∧
    twinPrimeCount 20000 < cousinPrimeCount 20000 ∧
    -- 交差 3: 20000→50000 で twin が cousin を再び追い越す
    cousinPrimeCount 20000 > twinPrimeCount 20000 ∧
    cousinPrimeCount 50000 < twinPrimeCount 50000

この 3 交差の命題は、本リポジトリ内では Lean により機械検証された事実である。

この振動的な大小関係は、双子素数と従兄弟素数が定数倍の意味で近似的に同程度の密度を持つという Hardy-Littlewood 予想（定数比 $C_4/C_2 = 1$ に近い）と整合している。

8.4 大スケール比較定理

/-- n=20000: twin(342) < cousin(344) < sexy(693) -/
theorem prime_gap_comparison_20000 :
    twinPrimeCount 20000 < cousinPrimeCount 20000 ∧
    cousinPrimeCount 20000 < sexyPrimeCount 20000

/-- n=50000: cousin(693) < twin(705) < sexy(1419) -/
theorem prime_gap_comparison_50000 :
    cousinPrimeCount 50000 < twinPrimeCount 50000 ∧
    twinPrimeCount 50000 < sexyPrimeCount 50000

特筆すべきは n=50000 における順序であり、twin が cousin をわずかに上回る（705 > 693）ことが精密に確認された。セクシー素数はすべてのスケールで twin と cousin の約 2 倍となっており、これも Hardy-Littlewood 定数の数値的予測（$C_6/C_2 \approx 2$）と整合する。

8.5 Admissibility 定理

Polignac 予想の「必要条件」として知られるタプル admissibility（$k$-tuple 予想の前提）を形式化した。

/-- {0,2}, {0,4}, {0,6} のすべてが admissible -/
theorem allSmallTuples_admissible :
    (∀ q : ℕ, Nat.Prime q → ∃ r < q, r % q ≠ 0 ∧ r % q ≠ 2 % q) ∧
    (∀ q : ℕ, Nat.Prime q → ∃ r < q, r % q ≠ 0 ∧ r % q ≠ 4 % q) ∧
    (∀ q : ℕ, Nat.Prime q → ∃ r < q, r % q ≠ 0 ∧ r % q ≠ 6 % q)

Admissibility は「$k$-tuple が無限に多く素数対を実現するための必要条件」であり（Hardy-Littlewood $k$-tuple 予想参照）、この定理は 3 種類の near-twin 族すべてがこの条件を満たすことを確認する。

9. 残存ブロッカーの分析

9.1 ブロッカー一覧

ブロッカー 種別 内容 解決予測
EHPaperInput.eh_exists 数学的未解決問題 EH 予想（θ > 1/2）の証明 未定
EHPaperInput.eh_to_twinPrimeCountBound Lean 外部形式化 Maynard 篩ブリッジの Lean 内実装 中期
ZhangPaperInput.zhang_bounded_gaps Lean 外部形式化 Zhang 定理の Lean4 内形式化 中長期
GapReductionInput.gap_reduction_to_twin Lean 外部形式化 EH ギャップ縮小の Lean 内実装 中長期

9.2 EH 予想の数学的難しさ

EH 予想が難しい根本理由は「大きなモジュラスに対する素数の等分布」という問いにある。

Bombieri-Vinogradov（BV）定理は θ < 1/2 の範囲を「均一な解析的数論」で解決する。BV の証明では Dirichlet L 関数の零点自由領域と密度定理が核心的役割を果たすが、θ = 1/2 で証明の手法が壁に突き当たる。

θ > 1/2 への拡張はリーマン予想（GRH）からも従わない。GRH は個々のモジュラスの L 関数の零点制御を与えるが、EH が要求する「すべてのモジュラスについての一様性」は GRH と独立な問いである。

9.3 Zhang 形式化の展望

[Zhang 2013] の篩論証は 50 ページ超の精密な解析的整数論であり、Lean4 での完全形式化は相当な工学的投資を要する。Lean4 Mathlib には現在：

  • Dirichlet L 関数の解析性（Mathlib 4.x で整備中）
  • Möbius 関数・篩の初等的 API
  • Selberg 篩の形式化（未完）

が存在する状況であり、Zhang 証明に必要な「Deligne-Fouvry-Friedlander 型の指数和評価」「型 II 和の推定」等は現時点で Mathlib に存在しない。

9.4 短期的に可能な前進

  1. admissibility の完全 Lean 形式化：twinPrimeTuple_admissible の一般化を Mathlib の Finset API で拡張
  2. 計算的カウントの拡張：$n = 100{,}000$ スケールへの native_decide 適用
  3. BV 定理の部分的 Lean 形式化：個別モジュラスの素数等分布補題から始めるボトムアップ実装
  4. Brun 定数の有限近似：$\sum_{p \le N, (p,p+2) \text{ twin}} 1/p$ の計算的下界

10. 関連問題との接続

10.1 Brun の定理との比較

Brun（1919）の定理：

$$B = \sum_{\substack{(p, p+2)\ p, p+2 \text{ 素数}}} \left(\frac{1}{p} + \frac{1}{p+2}\right) < \infty \approx 1.9021605\ldots$$

この有限性は「もし双子素数が無限にあるとしても、逆数和は収束する」ことを示す。本形式化では Brun 定数の計算的近似は実装していない。有限部分和の評価は、別途の数値計算スクリプトで扱う方針とする。

10.2 GPY 定理との関係

Goldston-Pintz-Yıldırım（2005/2009）は：

$$\liminf_{n \to \infty} \frac{p_{n+1} - p_n}{\log p_n} = 0$$

を証明した。本形式化には GPY の形式化は含まれないが、Infinitude.lean における「任意大きな小さいギャップが存在する」という主張の弱い形（特定スケールでの gap-2 密度）は計算的に証明されている。

10.3 Cramér 予想との比較

Cramér（1936）の予想：$\limsup_{n \to \infty} (p_{n+1} - p_n) / (\log p_n)^2 = 1$。これは最大ギャップに関する予想であり、最小ギャップ（双子素数）とは双対的な関係にある。本形式化のスコープ外だが、今後の BoundedGaps.lean 拡張で最大ギャップ下界の形式化が検討できる。

11. 議論と今後の方向性

11.1 形式化の到達評価

本形式化の主要な数学的貢献を以下に整理する。

機械検証済み内容（theorem=423, sorry=0, axiom=1）：

  • 双子素数の代数的構造（mod 6, mod 12）
  • 奇ギャップ不可能性
  • 計算的精密カウント（n ≤ 50,000 スケール）
  • 順位交差現象の形式的証明
  • Polignac admissibility（必要条件の確認）

条件付きで証明された内容（外部入力を型シグネチャで明示）：

  • TwinPrimeConjecture_conditional_EH（EH 条件付き）
  • TwinPrimeConjecture_from_zhang_and_gap_reduction（Zhang + EH 条件付き）
  • TwinPrimeConjecture_from_EH_via_gaps（EH via gaps 条件付き）

未解決のまま明示的に保留：

  • EH 予想（θ > 1/2）の解決
  • Zhang 定理の Lean4 内部形式化

11.2 形式化手法としての意義

本形式化が示したことは、「形式化を通じた依存構造の可視化」の有用性である。

EHPaperInput という型を定義することで、「EH 予想 → 双子素数定理」という依存が Lean の型システムに刻まれた。今後 EH の Lean 形式化が完成した際、EHPaperInput のインスタンスを構成するだけで TwinPrimeConjecture が自動的に導出される。この仕組みは非形式的な引用関係では達成できない厳密さを持つ。

11.3 計算的側面の意義

「従兄弟素数が n=3000 で双子素数を追い越す」という事実は従来から経験的に知られていたが、Lean 4 による native_decide の証明は、この事実が Lean の型システムにより機械検証された最初の事例である可能性がある。計算的な定理は「実験的事実」から「証明された命題」への昇格を意味する。

11.4 今後の方向性

短期（3 か月以内）：

  1. n = 100,000 スケールの計算的カウントの追加
  2. Brun 定数の有限近似版補題の形式化
  3. prime_gap_comparison を任意のスケールで自動生成するメタ補題

中期（1 年以内）：

  1. Selberg 篩の Lean4 形式化（Mathlib PR として）
  2. Bombieri-Vinogradov の個別モジュラス版の形式化
  3. ZhangPaperInput を theorem に格上げするための Lean 証明

長期（3 年以内）：

  1. Maynard 篩の完全 Lean4 形式化
  2. EHPaperInput を theorem に格上げするための Lean 証明（EH の未解決性に依存）
  3. TwinPrimeConjecture の無条件 Lean 証明（EH 解決が前提）

参考文献

  1. V. Brun, "La série 1/5 + 1/7 + 1/11 + 1/13 + ... est convergente ou finie," Bulletin des Sciences Mathématiques, 43:100–104, 124–128, 1919.

  2. P.D.T.A. Elliott and H. Halberstam, "A conjecture in prime number theory," Symposia Mathematica, 4:59–72, 1968.

  3. D. A. Goldston, J. Pintz, and C. Y. Yıldırım, "Primes in Tuples I," Annals of Mathematics, 170(2):819–862, 2009.

  4. G. H. Hardy and J. E. Littlewood, "Some problems of 'Partitio Numerorum'; III: On the expression of a number as a sum of primes," Acta Mathematica, 44:1–70, 1923.

  5. J. Maynard, "Small gaps between primes," Annals of Mathematics, 181(1):383–413, 2015.

  6. A. de Polignac, "Six propositions arithmologiques déduites du crible d'Ératosthène," Nouvelles Annales de Mathématiques, 8:423–429, 1849.

  7. D. H. J. Polymath, "Variants of the Selberg sieve, and bounded intervals containing many primes," Research in the Mathematical Sciences, 1(12), 2014.

  8. Y. Zhang, "Bounded gaps between primes," Annals of Mathematics, 179(3):1121–1174, 2013.

  9. The Mathlib Community, "The Lean 4 Mathematical Library," Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024.

  10. OEIS, "A007508: Number of twin prime pairs (p, p+2) with p < 10^n," The On-Line Encyclopedia of Integer Sequences, https://oeis.org/A007508.

付録：形式化進捗の機械再現手順

環境要件

lean-toolchain: leanprover/lean4:v4.27.0
lake: bundled with lean4
OS: macOS / Linux

ビルド再現

cd /path/to/research-app
lake build TwinPrimes

注記（2026-05-19 再現実行）：

  • この実行では TwinPrimes.EHConditional で Lean exit code 139 が発生し、exit=1 となった。
  • 詳細ログは articles/TwinPrimes_Attachments_2026-05-19/06_Build_Verification_2026-05-19.md を参照。

SSOT 計測再現

cd /path/to/research-app
python3 -c "
import sys, datetime
sys.path.insert(0, '.')
from framework.lean_measurement import scan_lean_tree
from datetime import timezone

r = scan_lean_tree('.', path='framework/lean4/TwinPrimes')
ts = datetime.datetime.now(timezone.utc).isoformat()
print(f'Measured: {ts}')
print(f'sorry={len(r[\"sorries\"])}')
print(f'axiom={len(r[\"axioms\"])}')
print(f'theorem={r[\"theorem_count\"]}')
print(f'lines={r[\"total_lines\"]}')
print(f'files={r[\"files_scanned\"]}')
"
# 期待出力（2026-05-19 計測値）:
# sorry: 0   axiom: 1   theorem: 423   lines: 3963

個別定理の検証例

# EH 条件付き証明チェーンの確認
grep -n "TwinPrimeConjecture_conditional_EH\|TwinPrimeConjecture_from_zhang" \
     framework/lean4/TwinPrimes/EHConditional.lean \
     framework/lean4/TwinPrimes/BoundedGaps.lean

# 交差現象定理の確認
grep -n "twin_cousin_crossing_events" \
     framework/lean4/TwinPrimes/BoundedGaps.lean

# 計算的カウントの確認
grep -n "native_decide\|decide" \
     framework/lean4/TwinPrimes/Structural.lean | head -20

個別補題の型確認

# Lean4 REPL での確認
lake repl
-- #check TwinPrimes.BoundedGaps.TwinPrimeConjecture_from_zhang_and_gap_reduction
-- #check TwinPrimes.EHConditional.TwinPrimeConjecture_conditional_EH
-- #check TwinPrimes.BoundedGaps.twin_cousin_crossing_events
-- #check TwinPrimes.BoundedGaps.polignac_consistency_k246
0
0
0

Register as a new user and use Qiita more conveniently

  1. You get articles that match your needs
  2. You can efficiently read back useful information
  3. You can use dark theme
What you can do with signing up
Sign upLogin
0
0

Delete article

Deleted articles cannot be recovered.

Draft of this article would be also deleted.

Are you sure you want to delete this article?