Andrica's Conjecture — A Lean 4 Mathlib-Native Treatment with Structural Sufficient Conditions

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

• Zenodo (DOI, canonical): https://doi.org/10.5281/zenodo.19646836
• Internet Archive: https://archive.org/details/rei-aios-paper-116-1776560994796
• Harvard Dataverse: https://doi.org/10.7910/DVN/KC56RY
• GitHub source (private): https://github.com/fc0web/rei-aios Author: Nobuki Fujimoto (@fc0web) · ORCID 0009-0004-6019-9258 · License CC-BY-4.0 ---

Authors: Nobuki Fujimoto (ORCID 0009-0004-6019-9258), Claude Code (Lean 4 formalization)
Date: 2026-04-19
Status: DRAFT — partial formalization, not a proof of the full conjecture.
License: CC-BY-4.0
Repository: fc0web/rei-aios
Key file: data/lean4-mathlib/CollatzRei/AndricaConjecture.lean (33 theorems, 0 sorry)
Related: Paper 74 (Andrica quadratic-log bound), STEP 701 (Lean 4 skeleton).

Abstract

Andrica's conjecture (1985) asserts A_n = √p_{n+1} − √p_n < 1 for every n ≥ 1, where p_n denotes the n-th prime. The conjecture is empirically verified for n ≤ 1.3 × 10^16 but remains open. We provide a Mathlib-native Lean 4 formalization with 33 zero-sorry theorems: 24 concrete cases for n = 1, ..., 24 (primes 2 through 97) via decide, the extremal case n = 4 (p = 7, q = 11) with exact margin 12, and three structural sufficient conditions that prove Andrica for any consecutive-prime pair under restrictions on the prime gap.

We use an integer-squared form (q − p)² < 4p + 1 which implies the original bound since 4√p + 1 ≥ 1. All proofs are elementary (decide, omega, Nat.mul_le_mul). The formalization upgrades STEP 701 (which was self-contained / no Mathlib) to a Mathlib v4.27.0 file using Nat.Prime.

No new proof of the full conjecture. The structural sufficient conditions are upper-bounded by finitely-tracked prime-gap regimes (gap ≤ 4 at p ≥ 5 and gap ≤ 6 at p ≥ 10). An unconditional treatment of arbitrary gaps requires external prime-gap estimates (Baker-Harman-Pintz 2001: gap < p^0.525 for large p).

Keywords: Andrica's conjecture, prime gaps, Lean 4, Mathlib, formal verification.

1. Background

1.1 Andrica 1985

Let p_n denote the n-th prime. Andrica conjectured

A_n := √p_{n+1} − √p_n < 1       for all n ≥ 1

Equivalently, the prime gap g_n = p_{n+1} − p_n satisfies

g_n < 2√p_n + 1.

Verification: n ≤ 1.3 × 10^16 (Oliveira e Silva, 2014+).

1.2 Key numerical features

• Max of A_n occurs at n = 4: A_4 = √11 − √7 ≈ 0.6709.
• For n ≥ 30, empirically A_n → 0 as n → ∞ (Cramér heuristics predict g_n = O((log p_n)²)).
• The conjecture follows from Cramér's conjecture (unproved).

1.3 Known prime-gap bounds

• Baker-Harman-Pintz (2001): g_n < p_n^0.525 for sufficiently large n.
• Under Riemann hypothesis: g_n = O(p_n^0.5 · log p_n).
• Empirically: g_n = O((log p_n)²).

2. Lean 4 formalization (this paper)

File: data/lean4-mathlib/CollatzRei/AndricaConjecture.lean. 33 theorems, 0 sorry, Mathlib v4.27.0.

2.1 Integer-squared form

Squaring the Andrica inequality and clearing (√): g² < 4p + 4√p + 1. Since 4√p + 1 ≥ 1, a sufficient condition is

(q − p)² < 4p + 1       (integer arithmetic)

This is the form we formalize:

def andricaInt (p q : Nat) : Prop :=
  (q - p) * (q - p) < 4 * p + 1

2.2 Concrete small cases (24 theorems)

For each of the first 24 consecutive prime pairs (p, q):

All proved by decide. The extremal case n = 4 has exact margin 4·7 + 1 − 16 = 13; actual 4·7 − 16 = 12 is the raw margin.

2.3 Structural sufficient conditions

Three elementary lemmas that handle infinite families of gap-bounded pairs:

theorem andrica_small_gap    (p q : Nat) (hp : 5  ≤ p) (hq : q - p ≤ 4) : andricaInt p q
theorem andrica_moderate_gap (p q : Nat) (hp : 10 ≤ p) (hq : q - p ≤ 6) : andricaInt p q
theorem andrica_via_gap_squared_le_4p (p q : Nat) (h : (q-p)² ≤ 4p) : andricaInt p q

Proofs use Nat.mul_le_mul hq hq for the gap² bound and omega for the final arithmetic. Together they cover:

• All pairs with gap ≤ 4 and p ≥ 5 (covers the bulk of small primes).
• All pairs with gap ≤ 6 and p ≥ 10.
• All pairs with the more general condition gap² ≤ 4p (arbitrary gap relative to p).

2.4 Primality cross-checks

Mathlib Nat.Prime evaluations for witnesses:

theorem seven_prime : Nat.Prime 7 := by decide
theorem eleven_prime : Nat.Prime 11 := by decide
theorem ninety_seven_prime : Nat.Prime 97 := by native_decide

3. Summary theorem

theorem Andrica_summary :
    andricaInt 7 11
    ∧ (∀ p q, 5 ≤ p → q - p ≤ 4 → andricaInt p q)
    ∧ (∀ p q, 10 ≤ p → q - p ≤ 6 → andricaInt p q)
    ∧ (∀ p q, (q - p) * (q - p) ≤ 4 * p → andricaInt p q)

4. Scope and limitations

What this paper does

1. 24 concrete consecutive-prime cases through n = 24 verified via decide.
2. Extremal case n = 4 identified with explicit margin.
3. Three sufficient-condition lemmas covering infinite families.
4. Mathlib v4.27.0 native — uses Nat.Prime for primality.

What this paper does not

1. Does not prove the full conjecture. Covers pairs where the gap is bounded (≤ 4, ≤ 6, or more generally gap² ≤ 4p).
2. Does not handle very large gaps. For asymptotic bounds one would need Baker-Harman-Pintz (p_n^0.525) or Cramér (log² p) conjectures.
3. No new number-theoretic result. The integer form (q-p)² < 4p+1 is standard; the contribution is Lean 4 formalization.

Honest claim

The 33-theorem Lean 4 file is a complete formalization of what is elementary about Andrica's conjecture: (i) small cases, (ii) gap-bounded sufficient conditions, (iii) the extremal pair. Closing the conjecture unconditionally remains open.

5. Connection to Paper 74

Paper 74 (Andrica quadratic-log bound, earlier Rei paper) proposed a structural g ≤ 2√p view. The present paper formalizes a closely-related sufficient condition (g² < 4p+1) in Lean 4. The two are compatible: g² ≤ 4p ⟹ g ≤ 2√p ⟹ Andrica.

6. Reproducibility

• data/lean4-mathlib/CollatzRei/AndricaConjecture.lean
  • Build: cd data/lean4-mathlib && lake build CollatzRei.AndricaConjecture
  • 33 theorems, 0 sorry, builds in ~6s against Mathlib v4.27.0

7. Future work

1. Paper 117: Erdős-Straus Mathlib formalization (parallel treatment, already drafted).
2. Paper 118 candidate: extend sufficient conditions using Baker-Harman-Pintz asymptotic bound (would require Mathlib analytic-number-theory API, currently thin).
3. Integrate with Rei Ricci-flow category classification (Paper 108): Andrica gives 100% Category E (explosive) — Paper 116 is consistent with this characterization.

Paper 116 draft prepared 2026-04-19 by Claude Code under Nobuki Fujimoto's direction. This is an elementary formalization paper, not a claim of proof. Rei-AIOS research programme.