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

Erdős Problem 295

Reference: erdosproblems.com/295

Imports (1)
Imported by 1 file
  1. lemma Erdos295.exists_k Helper lemma: for each $N$, there exists $k$ and $n_1 < ... < n_k$ such that $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$ sorry line 37 source

    Source documentation

    Helper lemma: for each $N$, there exists $k$ and $n_1 < ... < n_k$ such that $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$.

    depends on sorry what this means

    Statement uses: Nat, Exists, Fin, And, LE.le, StrictMono, Eq, Real, Finset.sum, Finset.univ, HDiv.hDiv, OfNat.ofNat

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

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    lemma exists_k (N : ℕ) : ∃ (k : ℕ) (n : Fin k → ℕ),
    (∀ i, N ≤ n i) ∧ StrictMono n ∧ ∑ i, (1 / n i : ℝ) = 1 := by
…

    Mentions: Erdos295.k

  2. abbrev Erdos295.k Let $k(N)$ denote the smallest $k$ such that there exists $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$ line 45 source

    Source documentation

    Let $k(N)$ denote the smallest $k$ such that there exists $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$.

    depends on sorry what this means

    Statement uses: Nat

    Proof uses: Nat.find, Exists, Fin, And, LE.le, StrictMono, Eq, Real, Finset.sum, Finset.univ, HDiv.hDiv, OfNat.ofNat, Classical.propDecidable, Erdos295.exists_k

    13 instances, coercions and auxiliary constants left out.

    noncomputable abbrev k (N : ℕ) : ℕ :=
…
  3. theorem Erdos295.erdos_295 Documented declaration: erdos_295 sorry line 57 source

    Source documentation

    Let $k(N)$ denote the smallest $k$ such that there exists $N ≤ n_1 < ⋯ < n_k$ with $\frac 1 {n_1} + ... + \frac 1 {n_k} = 1$

    Is it true that $\lim_{N \to \infty} k(N) - (e - 1)N = \infty$?

    depends on sorry what this means

    Statement uses: Iff, True, Filter.Tendsto, Nat, Real, HSub.hSub, Erdos295.k, HMul.hMul, Real.exp, OfNat.ofNat, Filter.atTop

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

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_295 :
    answer(sorry) ↔ Filter.atTop.Tendsto (fun N => k N - (rexp 1 - 1)*N) Filter.atTop := by
…

    Mentions: Erdos295.k

  4. theorem Erdos295.erdos_295.variants.erdos_straus Erdős and Straus have proved the existence of some constant $c>0$ such that $-c < k(N)-(e-1)N \ll \frac N {\log N}$ sorry line 66 source

    Source documentation

    Erdős and Straus have proved the existence of some constant $c>0$ such that $-c < k(N)-(e-1)N \ll \frac N {\log N}$

    depends on sorry what this means

    Statement uses: Exists, Real, And, GT.gt, OfNat.ofNat, Filter.Eventually, Nat, Membership.mem, Set, Set.Ioc, Neg.neg, HDiv.hDiv, HMul.hMul, Real.log, HSub.hSub, Erdos295.k, Real.exp, Filter.atTop

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

    37 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_295.variants.erdos_straus :
    ∃ᵉ (C > 0) (O > 0), ∀ᶠ (N : ℕ) in Filter.atTop,
      (k N - (rexp 1 - 1)*N) ∈ Set.Ioc (-C) (O * N / (N : ℝ).log):= by
…

    Mentions: Erdos295.k