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

Reference: erdosproblems.com/257

Imports (1)
  1. theorem Erdos257.erdos_257 Let $A\subseteq\mathbb{N}$ be an infinite set sorry line 38 source

    Source documentation

    Let $A\subseteq\mathbb{N}$ be an infinite set. Is $$ \sum_{n\in A} \frac{1}{2^n - 1} $$ irrational?

    depends on sorry what this means

    Statement uses: Iff, True, Set, Nat, Set.Infinite, Irrational, tsum, Real, HDiv.hDiv, OfNat.ofNat, HSub.hSub, HPow.hPow, Membership.mem, SummationFilter.unconditional

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

    46 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_257 : answer(sorry) ↔ ∀ (A : Set ℕ), A.Infinite →
    Irrational (∑' n : A, (1 : ℝ) / (2 ^ n.1 - 1)) := by
…
  2. theorem Erdos257.erdos_257.variants.tsum_top_eq Show that $$ \sum_{n} \frac{1}{2^n - 1} = \sum_{n} \frac{d(n)}{2^n}, $$ where $d(n)$ is the number of divisors of $n$ line 50 source

    Source documentation

    Show that $$ \sum_{n} \frac{1}{2^n - 1} = \sum_{n} \frac{d(n)}{2^n}, $$ where $d(n)$ is the number of divisors of $n$.

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

    Statement uses: Eq, Real, tsum, Nat, HDiv.hDiv, OfNat.ofNat, HSub.hSub, HPow.hPow, SummationFilter.unconditional, Finset.card, Nat.divisors

    Proof uses: LT.lt, Norm.norm, of_eq_true, Eq.trans, True, Mathlib.Meta.NormNum.instAtLeastTwo, congrFun', congrArg, Mathlib.Meta.NormNum.IsNNRat.to_eq, Mathlib.Meta.NormNum.isNNRat_div, Mathlib.Meta.NormNum.isNNRat_mul, HMul.hMul, Inv.inv, Eq.refl, Mathlib.Meta.NormNum.IsNat.to_isNNRat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Meta.NormNum.isNNRat_inv_pos, Nat.mul, norm_div and 176 more

    206 instances, coercions and auxiliary constants left out.

    Tactic trace: 41 steps

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

    theorem erdos_257.variants.tsum_top_eq :
    ∑' n, 1 / (2 ^ n - 1 : ℝ) = ∑' n, n.divisors.card / (2 ^ n : ℝ) := by
…
  3. theorem Erdos257.erdos_257.variants.tsum_top sorry line 100 source

    depends on sorry what this means

    Statement uses: Irrational, tsum, Real, Nat, HDiv.hDiv, Finset.card, Nat.divisors, HPow.hPow, OfNat.ofNat, SummationFilter.unconditional

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

    34 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  4. theorem Erdos257.erdos_257.variants.summable_reciprocal_support sorry line 121 source

    depends on sorry what this means

    Statement uses: Nat, Set, LE.le, OfNat.ofNat, Set.Infinite, Summable, Real, HDiv.hDiv, Membership.mem, SummationFilter.unconditional, Irrational, tsum, HSub.hSub, HPow.hPow

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

    44 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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