FormalConjectures/ErdosProblems/968.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

6 declarations, 5 contain sorry, 0 declared as axioms

Erdős Problem 968

Let uₙ = pₙ / n, where pₙ is the nth prime. Does the set of n such that uₙ < uₙ₊₁ have positive lower density?

Erdős and Prachar also proved that ∑_{pₙ < x} |uₙ₊₁ - uₙ| ≍ (log x)^2, and that the set of n such that uₙ > uₙ₊₁ has positive lower density. Erdős also asked whether there are infinitely many increasing triples uₙ < uₙ₊₁ < uₙ₊₂ or decreasing triples uₙ > uₙ₊₁ > uₙ₊₂.

Reference: erdosproblems.com/968

[ErPr61] Erdős, P. and Prachar, K., Sätze und Probleme über pₖ/k. Abh. Math. Sem. Univ. Hamburg (1961/62), 251–256.

[FMT18] Ford, K. and Maynard, J. and Tao, T., Chains of large gaps between primes. Irregularities in the distribution of prime numbers, Springer (2018), 1–21.

[Ma15] Maynard, J., Small gaps between primes. Ann. of Math. (2015), 383–413.

Imports (1)
Imported by 1 file
  1. def Erdos968.u u n is the normalized nth prime, defined as pₙ / (n+1) where pₙ is the nth prime (with 0.nth Nat.Prime = 2) line 55 source

    Source documentation

    u n is the normalized nth prime, defined as pₙ / (n+1) where pₙ is the nth prime (with 0.nth Nat.Prime = 2).

    This corresponds to the classical sequence (p₁/1, p₂/2, p₃/3, ...) while using Nat.nth Prime's 0-based indexing; in particular, the denominator is always positive.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Real

    Proof uses: HDiv.hDiv, Nat.nth, Nat.Prime, HAdd.hAdd, OfNat.ofNat

    9 instances, coercions and auxiliary constants left out.

    noncomputable def u (n : ℕ) : ℝ :=
…
  2. theorem Erdos968.erdos_968 Does the set {n | u n < u (n+1)} have positive lower density? sorry line 62 source

    Source documentation

    Does the set {n | u n < u (n+1)} have positive lower density?

    depends on sorry what this means

    Statement uses: Iff, True, LT.lt, Real, OfNat.ofNat, Set.lowerDensity, Nat, Set.ofPred, Erdos968.u, HAdd.hAdd, Set.univ

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_968 : answer(sorry) ↔ 0 < {n : ℕ | u n < u (n + 1)}.lowerDensity := by
…

    Mentions: Erdos968.u

  3. theorem Erdos968.erdos_968.variants.sum_abs_diff_isTheta_log_sq Erdős and Prachar proved ∑_{pₙ < x} |u (n+1) - u n| ≍ (log x)^2 (see [ErPr61]) sorry line 71 source

    Source documentation

    Erdős and Prachar proved ∑_{pₙ < x} |u (n+1) - u n| ≍ (log x)^2 (see [ErPr61]).

    We encode ∑_{pₙ < x} as a sum over n < Nat.primeCounting' x (the number of primes < x).

    depends on sorry what this means

    Statement uses: Asymptotics.IsTheta, Nat, Real, Filter.atTop, Finset.sum, Finset.Iio, Nat.primeCounting', abs, HSub.hSub, Erdos968.u, HAdd.hAdd, OfNat.ofNat, HPow.hPow, Real.log

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_968.variants.sum_abs_diff_isTheta_log_sq :
    (fun x : ℕ =>
        ∑ n < Nat.primeCounting' x, |u (n + 1) - u n|) =Θ[atTop]
      fun x : ℕ => log x ^ 2 := by
…

    Mentions: Erdos968.u

  4. theorem Erdos968.erdos_968.variants.decreasing_steps_pos_lower_density Erdős and Prachar proved that the set {n | u n > u (n+1)} has positive lower density (see [ErPr61]) sorry line 82 source

    Source documentation

    Erdős and Prachar proved that the set {n | u n > u (n+1)} has positive lower density (see [ErPr61]).

    depends on sorry what this means

    Statement uses: LT.lt, Real, OfNat.ofNat, Set.lowerDensity, Nat, Set.ofPred, GT.gt, Erdos968.u, HAdd.hAdd, Set.univ

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_968.variants.decreasing_steps_pos_lower_density :
    0 < {n : ℕ | u n > u (n + 1)}.lowerDensity := by
…

    Mentions: Erdos968.u

  5. theorem Erdos968.erdos_968.variants.infinite_increasingTriples Erdős asked whether there are infinitely many solutions to uₙ < uₙ₊₁ < uₙ₊₂ sorry line 95 source

    Source documentation

    Erdős asked whether there are infinitely many solutions to uₙ < uₙ₊₁ < uₙ₊₂.

    The answer is yes. Since uₙ < uₙ₊₁ is equivalent to pₙ₊₁ - pₙ > pₙ / n, it suffices to have infinitely many n with two consecutive prime gaps larger than pₙ / n ∼ log n. Ford, Maynard, and Tao [FMT18] proved that for every fixed k there are infinitely many n with k consecutive prime gaps all of size ≫ log pₙ · log log pₙ · log log log log pₙ / log log log pₙ.

    depends on sorry what this means

    Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, And, LT.lt, Real, Erdos968.u, HAdd.hAdd, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_968.variants.infinite_increasingTriples :
    answer(True) ↔ {n : ℕ | u n < u (n + 1) ∧ u (n + 1) < u (n + 2)}.Infinite := by
…

    Mentions: Erdos968.u

  6. theorem Erdos968.erdos_968.variants.infinite_decreasingTriples Erdős asked whether there are infinitely many solutions to uₙ > uₙ₊₁ > uₙ₊₂ sorry line 107 source

    Source documentation

    Erdős asked whether there are infinitely many solutions to uₙ > uₙ₊₁ > uₙ₊₂.

    The answer is yes. Since uₙ > uₙ₊₁ is equivalent to pₙ₊₁ - pₙ < pₙ / n, it suffices to have infinitely many n with pₙ₊₂ - pₙ bounded, because pₙ / n → ∞. Maynard [Ma15] proved that liminf (pₙ₊₂ - pₙ) < ∞.

    depends on sorry what this means

    Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, And, GT.gt, Real, Erdos968.u, HAdd.hAdd, OfNat.ofNat

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    8 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_968.variants.infinite_decreasingTriples :
    answer(True) ↔ {n : ℕ | u n > u (n + 1) ∧ u (n + 1) > u (n + 2)}.Infinite := by
…

    Mentions: Erdos968.u