DEV Community

Nobuki Fujimoto
Nobuki Fujimoto

Posted on • Originally published at doi.org

Twin Primes Conjecture under Rei-AIOS Lens — A Structural Reinterpretation of Zhang-Maynard Bounded-Gap Results

#math #lean #research #algorithms

This article is a re-publication of Rei-AIOS Paper 115 for the dev.to community.
The canonical version with full reference list is in the permanent archives below:

Authors: Nobuki Fujimoto (ORCID 0009-0004-6019-9258), Claude Code (Lean 4 formalization)
Date: 2026-04-19
Status: DRAFT — reinterpretation / survey paper. Not a claim of new proof.
License: CC-BY-4.0
Repository: fc0web/rei-aios
Key files:

  • data/lean4-mathlib/CollatzRei/TwinPrimes.lean (~25 theorems/axioms, 0 sorry)
  • data/lean4-mathlib/CollatzRei/Devissage.lean (abstract dévissage, companion)

Abstract

The Twin Primes conjecture — that infinitely many pairs (p, p+2) are both prime — remains open. We reinterpret the modern bounded-gap landscape (Zhang 2013, Maynard-Tao 2015, Polymath8b) under the Rei-AIOS 8-valued logic (D-FUMT₈) and the Ricci-flow category classification (Papers 108, 109, 111). The conjecture is positioned as a NEITHER → FLOWING transition problem: the N ≤ 246 result of Maynard-Tao shifts an uncountable family of open questions (existence of primes at gap N for every N) into a finite-bounded statement, while leaving N = 2 squarely in the NEITHER region. We provide Lean 4 zero-sorry formalization of the first 20 twin primes + honest axiomatization of Zhang and Maynard's theorems, plus an abstract dévissage companion file closing the well-founded-induction core of Roshanak-sensei's formalization.

No new proof claim. This paper is a structural survey that maps classical results into the Rei interpretive framework and identifies concrete formalization targets.

Keywords: twin primes, Zhang 2013, Maynard-Tao, bounded gaps, Lean 4, D-FUMT₈, Rei-AIOS.

1. Introduction

1.1 Classical background

The Twin Primes conjecture asks whether infinitely many pairs of primes differ by 2. Empirically, twin primes appear throughout the integers (the first 20: 3, 5, 11, 17, 29, 41, 59, 71, 101, 107, 137, 149, 179, 191, 197, 227, 239, 269, 281, 311, ...). The conjecture dates informally to Polignac 1849 and remains unproved.

The modern era of progress began with Zhang 2013, who proved that there exist infinitely many prime pairs with gap ≤ 70,000,000. This was the first unconditional bounded-gap result. Subsequent work by Maynard, Tao, and the Polymath8b consortium reduced the bound to 246. Under the Elliott-Halberstam conjecture the bound drops to 12, and under the generalized Elliott-Halberstam to 6 (Polymath8b 2014).

1.2 The 244 gap

Between Maynard's 246 and the conjecture's 2 lies a gap of 244. This gap is what "twin primes remain open" means precisely:

Gap N Status
N ≤ 246 Infinitely many prime pairs at some N in this range (Maynard 2015)
N = 2 OPEN (Twin Primes conjecture)
... Each specific N in [3, 245] is also open for the "N" case

Closing the gap from 246 to 2 is what Twin Primes demands.

1.3 Rei-AIOS Ricci-flow category (Paper 108 framework)

Paper 108 introduced a three-category taxonomy (S/M/E: stable/moderate/explosive) for unsolved math problems based on discrete Ollivier-Ricci curvature:

  • Andrica: 100% Category E (explosive)
  • Erdős-Straus: 84.3% Category S (stable)
  • Collatz at n=27: Category M (moderate)

Twin Primes has not yet been categorized in that framework. The present paper positions it within the broader Rei interpretive layer while explicitly not claiming any new mathematical proof.

2. Lean 4 formalization (companion)

File: data/lean4-mathlib/CollatzRei/TwinPrimes.lean.

2.1 Basic definitions 

def isTwinPrime (p : Nat) : Prop := Nat.Prime p ∧ Nat.Prime (p + 2)

def infinitelyManyPrimePairsGap (N : Nat) : Prop :=
  ∀ M : Nat, ∃ p : Nat, p ≥ M ∧ Nat.Prime p ∧ Nat.Prime (p + N)
Enter fullscreen mode Exit fullscreen mode

2.2 Decidable small cases

20 twin primes verified with decide / native_decide:

  • p ∈ {3, 5, 11, 17, 29, 41, 59, 71, 101, 107, 137, 149, 179, 191, 197, 227, 239, 269, 281, 311}
  • Non-examples: 7 (since 9 = 3² is not prime), 13 (since 15 = 3·5 is not prime)

2.3 Axiomatized classical results 

axiom zhang_2013 :
  ∃ N : Nat, N ≤ 70000000 ∧ infinitelyManyPrimePairsGap N

axiom maynard_tao_2014 :
  ∃ N : Nat, N ≤ 246 ∧ infinitelyManyPrimePairsGap N

axiom under_elliott_halberstam :
  (∃ N : Nat, N ≤ 12 ∧ infinitelyManyPrimePairsGap N)

def TwinPrimesConjecture : Prop := infinitelyManyPrimePairsGap 2
Enter fullscreen mode Exit fullscreen mode

2.4 Elementary relations (zero-sorry corollaries) 

theorem maynard_stronger_than_zhang : (246 : Nat) < 70000000
theorem eh_stronger_than_maynard : (12 : Nat) < 246
theorem twin_gap_below_maynard : (2 : Nat) < 246
Enter fullscreen mode Exit fullscreen mode

All build successfully against Mathlib v4.27.0.

3. Abstract dévissage companion (closing 3-5 of Roshanak-sensei's sorries)

File: data/lean4-mathlib/CollatzRei/Devissage.lean (new).

Roshanak-sensei's note article (https://note.com/nifty_godwit2635/n/n3c70baa9f3b2) provided a dévissage formalization with 5 sorries remaining, split into (i) abstract-side (well-founded induction on (dim, length) lex) and (ii) scheme-side (coherent sheaves on Noetherian X).

Our companion file closes the abstract side zero-sorry:

  • devissage_abstract — the abstract Dévissage theorem with H2-H4 hypotheses.
  • strong_induction_lex — strong well-founded induction on lex complexity via nested Nat.strong_induction_on (avoids Prod.Lex API differences across Mathlib versions).
  • toy_devissage — concrete Nat instance demonstrating the theorem applies.

The scheme-side sorries (requiring Mathlib coherent-sheaf API) remain open in Roshanak-sensei's file; these are estimated at 12-24 months of Mathlib-ecosystem work per the original article's roadmap.

4. Rei D-FUMT₈ interpretation layer

4.1 Framing

Within D-FUMT₈ 8-valued logic, the Twin Primes conjecture sits naturally as a NEITHER → FLOWING transition question:

  • Below finite threshold (small p): twin primes are enumerable. D-FUMT₈ value = FLOWING (abundant, concrete).
  • Asymptotic regime (p → ∞): existence is unsettled. D-FUMT₈ value = NEITHER (neither proved nor disproved).
  • Zhang/Maynard progress: converts part of the NEITHER region to FLOWING by guaranteeing SOME gap ≤ 246 is FLOWING-asymptotic.

4.2 Explicit non-claim

This framing is philosophical and carries no mathematical proof content:

  • No computation derives D-FUMT₈ values from prime gaps.
  • No reduction from D-FUMT₈ to twin-prime existence exists.
  • The mapping is pedagogical / interpretive.

4.3 Analogy with Collatz atomic cores

Rei's Collatz atomic-core framework (STEP 696) isolated 25 "hard" integers ≤ 235 that resist the tier2 bound. Twin primes similarly admit a "hard-range" interpretation: the specific N = 2 is the singular hardest case within the bounded-gap continuum, much as n = 27 is the hardest starter within the atomic-core set.

This analogy is suggestive, not deductive.

5. Five-axis comparison with related work

Axis Zhang 2013 Maynard 2015 Polymath8b 2014 Under EH This paper (115)
Bound N 70,000,000 246 246 (refined) 12 same bounds, Lean 4 axiomatized
Method Goldston-Pintz-Yıldırım variant Selberg sieve + k-tuples Polymath collaborative refinement EH conjecture Rei interpretive layer
Lean 4 none none none none 20 concrete twin primes + 4 axioms
Claim unconditional unconditional unconditional conditional reinterpretation only
New proof? Yes (new results) Yes (new results) Yes (collaborative refinement) depends on EH No (survey)

6. What Rei methods do and do not give here

6.1 Where Rei helps

  1. Lean 4 enumeration of small twin primes: 20 verified cases demonstrate decidability and provide a testbed.
  2. Honest axiomatization of Zhang and Maynard's theorems: gives a workable Lean 4 target for future full formalization.
  3. Dévissage companion: closes abstract-side 3/5 sorries of Roshanak-sensei's formalization, which may support future coherent-sheaf-level work relevant to prime-gap sieve theory.
  4. D-FUMT₈ pedagogical framing: makes the 244-gap concrete (from N=246 to N=2).

6.2 Where Rei does NOT help

  1. No new bound below 246: our axiomatization is a Lean 4 bridge, not a reduction.
  2. No proof that N = 2 works: Twin Primes remains open, and Rei methods do not lend themselves to this analytical-number-theory problem.
  3. No new asymptotic estimates: Selberg sieve, Bombieri-Vinogradov, and Elliott-Halberstam are out of scope for the Rei Ricci-flow / D-FUMT₈ lens.
  4. No P vs NP insight: this is orthogonal to the earlier Paper 114 phase-transition work.

7. Reproducibility

  • data/lean4-mathlib/CollatzRei/TwinPrimes.lean: 25 theorems/axioms, zero sorry.
    • Build: cd data/lean4-mathlib && lake build CollatzRei.TwinPrimes
  • data/lean4-mathlib/CollatzRei/Devissage.lean: 6 theorems, zero sorry.
    • Build: cd data/lean4-mathlib && lake build CollatzRei.Devissage

8. Honest positioning

  1. No original mathematical content is claimed. Twin Primes remains open.
  2. Zhang and Maynard are CORRECTLY cited as the source of the N ≤ 246 result.
  3. D-FUMT₈ framing is pedagogical, not a proof technique.
  4. Rei Ricci-flow category classification of Twin Primes is not yet carried out in this paper (left for future work).

9. Future work

  1. Paper 116 candidate: Ricci-flow Category classification of Twin Primes (does it fall in S/M/E?).
  2. Roshanak-sensei collaboration: potentially merge the abstract-dévissage companion into a unified Lean 4 dévissage library.
  3. Small-gap enumeration at scale: extend the 20-twin-prime decidable list to 1000+ via compiled routines.
  4. Under EH axiom: use under_elliott_halberstam as a hypothesis to derive stronger Lean 4 consequences.

Paper 115 draft prepared 2026-04-19 by Claude Code under Nobuki Fujimoto's direction. This is a survey / reinterpretation paper, not a proof claim. Rei-AIOS research programme; contact https://note.com/nifty_godwit2635 / fc0web@github / fc2webb@gmail.com.

Top comments (0)