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

Erdős Problem 267

Reference: erdosproblems.com/267

Imports (1)
  1. theorem Erdos267.erdos_267 Let $F_1=F_2=1$ and $F_{n+1} = F_n + F_{n-1}$ be the Fibonacci sequence sorry line 36 source

    Source documentation

    Let $F_1=F_2=1$ and $F_{n+1} = F_n + F_{n-1}$ be the Fibonacci sequence. Let $n_1 < n_2 < \dots$ be an infinite sequence with $\frac{n_{k+1}}{n_k} \ge c > 1$. Must $\sum_k \frac 1 {F_{n_k}}$ be irrational?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, Rat, GT.gt, OfNat.ofNat, StrictMono, LE.le, HDiv.hDiv, HAdd.hAdd, Irrational, tsum, Real, Nat.fib, SummationFilter.unconditional

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

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_267 : answer(True) ↔ ∀ᵉ (n : ℕ → ℕ) (c > (1 : ℚ)), StrictMono n → (∀ k, c ≤ n (k+1) / n k) →
    Irrational (∑' k, 1 / (Nat.fib <| n k)) := by
…

    Mentions: c

  2. theorem Erdos267.erdos_267.variants.generalisation_ratio_limit_to_infinity Let $F_1=F_2=1$ and $F_{n+1} = F_n + F_{n-1}$ be the Fibonacci sequence sorry line 46 source

    Source documentation

    Let $F_1=F_2=1$ and $F_{n+1} = F_n + F_{n-1}$ be the Fibonacci sequence. Let $n_1 < n_2 < \dots$ be an infinite sequence with $\frac {n_k}{k} \to \infty$. Must $\sum_k \frac 1 {F_{n_k}}$ be irrational?

    depends on sorry what this means

    Statement uses: Iff, True, Nat, StrictMono, Filter.Tendsto, Real, HDiv.hDiv, HAdd.hAdd, OfNat.ofNat, Nat.succ, Filter.atTop, Irrational, tsum, Nat.fib, SummationFilter.unconditional

    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: 1 steps

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

    theorem erdos_267.variants.generalisation_ratio_limit_to_infinity : answer(sorry) ↔ ∀ (n : ℕ → ℕ),
    StrictMono n → Filter.Tendsto (fun k => (n (k+1) / k.succ : ℝ)) Filter.atTop Filter.atTop →
    Irrational (∑' k, 1 / (Nat.fib <| n k)) := by
…
  3. theorem Erdos267.erdos_267.variants.specialization_pow_two sorry line 62 source

    depends on sorry what this means

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

    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: 1 steps

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

  4. theorem Erdos267.erdos_267.variants.fibonacci_inverse_sum The sum $\sum_n \frac 1 {F_{n}}$ itself was proved to be irrational by André-Jeannin sorry line 72 source

    Source documentation

    The sum $\sum_n \frac 1 {F_{n}}$ itself was proved to be irrational by André-Jeannin.

    Ref: André-Jeannin, Richard, Irrationalité de la somme des inverses de certaines suites récurrentes.

    depends on sorry what this means

    Statement uses: Irrational, tsum, Real, Nat, HDiv.hDiv, OfNat.ofNat, Nat.fib, SummationFilter.unconditional

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

    23 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

    theorem erdos_267.variants.fibonacci_inverse_sum :
    Irrational <| ∑' k, 1 / (Nat.fib k) := by
…