FormalConjectures/ErdosProblems/17.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, 3 contain sorry, 0 declared as axioms

Erdős Problem 17

Reference: erdosproblems.com/17

Imports (1)
Imported by 1 file
  1. def Erdos17.IsClusterPrime A prime $p$ is a cluster prime if every even natural number $n \le p - 3$ can be written as a difference of two primes $q_1 - q_2$ with $q_1, q_2 \le p$ line 34 source

    Source documentation

    A prime $p$ is a cluster prime if every even natural number $n \le p - 3$ can be written as a difference of two primes $q_1 - q_2$ with $q_1, q_2 \le p$.

    standard axioms: propext what this means

    Statement uses: Nat

    Proof uses: And, Nat.Prime, Even, LE.le, Int, HSub.hSub, OfNat.ofNat, Exists, Eq

    8 instances, coercions and auxiliary constants left out.

    def IsClusterPrime (p : ℕ) : Prop :=
…
  2. theorem Erdos17.erdos_17 Erdős Problem 17 sorry line 42 source

    Source documentation

    Erdős Problem 17. Are there infinitely many cluster primes?

    depends on sorry what this means

    Statement uses: Iff, True, Set.Infinite, Nat, Set.ofPred, Erdos17.IsClusterPrime

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

    1 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_17 : answer(sorry) ↔ {p : ℕ | IsClusterPrime p}.Infinite := by
…

    Mentions: Erdos17.IsClusterPrime

  3. def Erdos17.clusterPrimeCount The counting function of cluster primes $\le n$ line 46 source

    Source documentation

    The counting function of cluster primes $\le n$.

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

    Statement uses: Nat

    Proof uses: Nat.card, Set.ofPred, And, LE.le, Erdos17.IsClusterPrime

    2 instances, coercions and auxiliary constants left out.

    noncomputable def clusterPrimeCount (n : ℕ) : ℕ :=
…
  4. theorem Erdos17.erdos_17.variants.upper_BES In 1999 Blecksmith, Erdős, and Selfridge [BES99] proved the upper bound $$\pi^{\mathcal{C}}(x) \ll_A x(\log x)^{-A}$$ for every real $A > 0$ sorry line 56 source

    Source documentation

    In 1999 Blecksmith, Erdős, and Selfridge [BES99] proved the upper bound $$\pi^{\mathcal{C}}(x) \ll_A x(\log x)^{-A}$$ for every real $A > 0$.

    [BES99] Blecksmith, Richard and Erd\H os, Paul and Selfridge, J. L., Cluster primes. Amer. Math. Monthly (1999), 43--48.

    depends on sorry what this means

    Statement uses: Real, LT.lt, OfNat.ofNat, Asymptotics.IsBigO, Nat, Filter.atTop, Erdos17.clusterPrimeCount, HDiv.hDiv, HPow.hPow, Real.log

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

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_17.variants.upper_BES {A : ℝ} (hA : 0 < A) :
  (fun x ↦ (clusterPrimeCount x : ℝ)) =O[atTop] fun x ↦ x / (log x) ^ A := by
…

    Mentions: Erdos17.clusterPrimeCount

  5. theorem Erdos17.erdos_17.variants.upper_Elsholtz In 2003, Elsholtz [El03] refined the upper bound to $$\pi^{\mathcal{C}}(x) \ll x\,\exp\!\bigl(-c(\log\log x)^2\bigr)$$ for every real $0 < c < 1/8$ sorry line 68 source

    Source documentation

    In 2003, Elsholtz [El03] refined the upper bound to $$\pi^{\mathcal{C}}(x) \ll x\,\exp\!\bigl(-c(\log\log x)^2\bigr)$$ for every real $0 < c < 1/8$.

    [El03] Elsholtz, Christian, On cluster primes. Acta Arith. (2003), 281--284.

    depends on sorry what this means

    Statement uses: Exists, Real, And, LT.lt, OfNat.ofNat, Membership.mem, Set, Set.Ioo, HDiv.hDiv, Nat, Asymptotics.IsBigOWith, Filter.atTop, Erdos17.clusterPrimeCount, HMul.hMul, Real.exp, Neg.neg, HPow.hPow, Real.log

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

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_17.variants.upper_Elsholtz :
  ∃ C : ℝ, 0 < C ∧
    ∀ c ∈ Set.Ioo 0 (1 / 8),
      IsBigOWith C atTop (fun x ↦ (clusterPrimeCount x : ℝ))
        (fun x ↦ x * exp (-c * (log (log x)) ^ 2)) := by
…

    Mentions: c, Erdos17.clusterPrimeCount

  6. theorem Erdos17.isClusterPrime_97_isLeast_non_cluster $97$ is the smallest prime that is not a cluster prime line 77 source

    Source documentation

    $97$ is the smallest prime that is not a cluster prime.

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

    Statement uses: IsLeast, Nat, Set.ofPred, And, Nat.Prime, Not, Erdos17.IsClusterPrime, OfNat.ofNat

    Proof uses: Iff, Membership.mem, Finset, Finset.range, HSub.hSub, Even, Exists, HAdd.hAdd, LE.le, Iff.intro, Int, Eq, Decidable.byContradiction, Eq.mp, LT.lt, Exists.intro, And.intro, Eq.mpr, id, congrArg and 82 more

    92 instances, coercions and auxiliary constants left out.

    Tactic trace: 70 steps

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

    theorem isClusterPrime_97_isLeast_non_cluster : IsLeast {p : ℕ | p.Prime ∧ ¬ IsClusterPrime p} 97 := by
…

    Mentions: Erdos17.IsClusterPrime