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

Erdős Problem 287

Reference: erdosproblems.com/287

Imports (1)
  1. def Erdos287.max_gap The maximum gap between consecutive terms of a finite sequence s : Fin k → ℕ, i.e., $\max_{0 \le i < k-1} (s(i+1) - s(i))$ line 33 source

    Source documentation

    The maximum gap between consecutive terms of a finite sequence s : Fin k → ℕ, i.e., $\max_{0 \le i < k-1} (s(i+1) - s(i))$.

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

    Statement uses: Nat, Fin

    Proof uses: Finset.sup, HSub.hSub, OfNat.ofNat, Finset.univ, Fin.mk, HAdd.hAdd

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    def max_gap (k : ℕ) (s : Fin k → ℕ ) : ℕ  :=
…
  2. theorem Erdos287.erdos_287 Let $k\geq2$ sorry line 43 source

    Source documentation

    Let $k\geq2$. Is it true that, for any distinct integers $1 < n_1 < \cdots < n_k$ such that $\sum_{i=1}^k \frac{1}{n_i} = 1$, we must have $\max(n_{i+1} - n_i) \geq 3$?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, LE.le, OfNat.ofNat, Fin, StrictMono, LT.lt, Fin.mk, Eq, Real, Finset.sum, Finset.univ, HDiv.hDiv, Erdos287.max_gap

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

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    theorem erdos_287 : answer(sorry) ↔
    ∀ (k : ℕ) (hk : 2 ≤ k) (s : Fin k → ℕ),
    StrictMono s → 1 < s ⟨0, by omega⟩ →
    ∑ i : Fin k, 1/ (s i : ℝ) = 1 →
    3 ≤ max_gap k s:= by
…

    Mentions: Erdos287.max_gap

  3. theorem Erdos287.erdos_287.variants.gap_at_least_two sorry line 57 source

    depends on sorry what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Fin, StrictMono, LT.lt, Fin.mk, Eq, Real, Finset.sum, Finset.univ, HDiv.hDiv, Erdos287.max_gap

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

    32 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. theorem Erdos287.erdos_287.test.best_possible Documented declaration: best_possible line 70 source

    Source documentation

    The example $1 = \frac{1}{2}+\frac{1}{3}+\frac{1}{6}$ shows that $3$ would be best possible here: the sequence $(2, 3, 6)$ is a valid Egyptian fraction representation of $1$ with max_gap = 3.

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

    Statement uses: Fin, OfNat.ofNat, Nat, Matrix.vecCons, Matrix.vecEmpty, And, StrictMono, LT.lt, Eq, Real, Finset.sum, Finset.univ, HDiv.hDiv, Erdos287.max_gap

    Proof uses: And.intro, of_decide_eq_true, id, Bool, Decidable.decide, Bool.true, Eq.refl, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAddMonoidWithOne', congrFun', congrArg, HAdd.hAdd, Inv.inv, Finset.sum_congr, Finset, Membership.mem, one_div, Fin.sum_univ_three and 19 more

    76 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

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

    theorem erdos_287.test.best_possible :
    let s : Fin 3 → ℕ := ![2, 3, 6]
…
  5. theorem Erdos287.erdos_287.variants.prime_conjecture For all large $N$, there exists a prime $p \in [N, 2N]$ such that $\frac{p+1}{2}$ is also prime sorry line 91 source

    Source documentation

    For all large $N$, there exists a prime $p \in [N, 2N]$ such that $\frac{p+1}{2}$ is also prime.

    This is an open conjecture. If true, it would imply erdos_287 for all but at most finitely many exceptions (see erdos_287.variants.prime_conjecture_implies).

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Nat, LE.le, And, Nat.Prime, HMul.hMul, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd

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

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_287.variants.prime_conjecture : answer(sorry) ↔
    ∃ N₀ : ℕ, ∀ N : ℕ, N₀ ≤ N →
      ∃ p : ℕ, Nat.Prime p ∧ N ≤ p ∧ p ≤ 2 * N ∧ Nat.Prime ((p + 1) / 2) := by
…
  6. theorem Erdos287.erdos_287.variants.prime_conjecture_implies sorry line 108 source

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Nat, LE.le, And, Nat.Prime, HMul.hMul, OfNat.ofNat, HDiv.hDiv, HAdd.hAdd, Fin, StrictMono, LT.lt, Fin.mk, Eq, Real, Finset.sum, Finset.univ, Erdos287.max_gap

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

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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