FormalConjectures/ErdosProblems/1138.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

4 declarations, 1 contain sorry, 0 declared as axioms

Erdős Problem 1138

References:

Note that the conjecture has a claimed disproof found at: https://sourish-kumrawat.github.io/papers/Erdos_1138.pdf, see the discussion section on the Erdos problems website for more information.

Imports (1)
  1. def Erdos1138.sup_primeGap The maximal prime gap below $x$, i.e. $d(x) = \max_{p_n < x}(p_{n+1} - p_n)$, where $p_n$ denotes the $n$-th prime line 43 source

    Source documentation

    The maximal prime gap below $x$, i.e. $d(x) = \max_{p_n < x}(p_{n+1} - p_n)$, where $p_n$ denotes the $n$-th prime.

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

    Statement uses: Real, Nat

    Proof uses: Finset.sup, Finset.range, Nat.primeCounting', Nat.ceil, primeGap

    9 instances, coercions and auxiliary constants left out.

    noncomputable def sup_primeGap (x : ℝ) : ℕ := (Finset.range (primeCounting' ⌈x⌉₊)).sup primeGap

    Mentions: primeGap

  2. abbrev Erdos1138.snd_gt_half_fst The filter on $\mathbb{R} \times \mathbb{R}$ corresponding to sending $x \to \infty$ subject to $x/2 < y < x$ line 48 source

    Source documentation

    The filter on $\mathbb{R} \times \mathbb{R}$ corresponding to sending $x \to \infty$ subject to $x/2 < y < x$

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

    Statement uses: Filter, Prod, Real

    Proof uses: Min.min, Filter.comap, Prod.fst, Filter.atTop, Filter.principal, Set.ofPred, Membership.mem, Set, Set.Ioo, HDiv.hDiv, OfNat.ofNat, Prod.snd

    9 instances, coercions and auxiliary constants left out.

    abbrev snd_gt_half_fst : Filter (ℝ × ℝ) := atTop.comap Prod.fst ⊓ 𝓟 {p | p.2 ∈ Ioo (p.1 / 2) p.1}
  3. def Erdos1138.primeCount_Ioc_mul_const Given a pair $(x,y)$, this is the amount of primes in the interval above $y$, of length equalling the largest prime gap before $x$, scaled by a constant $C$ line 53 source

    Source documentation

    Given a pair $(x,y)$, this is the amount of primes in the interval above $y$, of length equalling the largest prime gap before $x$, scaled by a constant $C$.

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

    Statement uses: Real, Prod

    Proof uses: Erdos1138.primeCount_Ioc_mul_const.match_1, HSub.hSub, Nat.primeCounting, Nat.floor, HAdd.hAdd, HMul.hMul, Erdos1138.sup_primeGap

    14 instances, coercions and auxiliary constants left out.

    noncomputable def primeCount_Ioc_mul_const (C : ℝ) : (ℝ × ℝ) → ℝ :=
…
  4. theorem Erdos1138.erdos_1138 sorry line 64 source

    depends on sorry what this means

    Statement uses: Iff, False, Real, GT.gt, OfNat.ofNat, Asymptotics.IsEquivalent, Prod, Erdos1138.snd_gt_half_fst, Erdos1138.primeCount_Ioc_mul_const, Erdos1138.primeCount_Ioc_mul_const.match_1, HDiv.hDiv, HMul.hMul, Erdos1138.sup_primeGap, Real.log

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

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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