Skip to content

Erdős problem 267

Start work

If n1<n2<⋯n_1 < n_2 < \cdots with nk+1/nk≥c>1n_{k+1}/n_k \ge c > 1, must ∑k1/Fnk\sum_k 1/F_{n_k} be irrational? The proposed proof closes the range 1<c<21 < c < 2 left open by earlier criteria.

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

267.lean

Retained formal statement3 of 4

Let F1=F2=1F_1=F_2=1 and Fn+1=Fn+Fn−1F_{n+1} = F_n + F_{n-1} be the Fibonacci sequence. Let n1<n2<…n_1 < n_2 < \dots be an infinite sequence with nkk→∞\frac {n_k}{k} \to \infty. Must ∑k1Fnk\sum_k \frac 1 {F_{n_k}} be irrational?

FormalConjectures/ErdosProblems/267.leanErdos267.erdos_267.variants.generalisation_ratio_limit_to_infinity5 linesExact file
True ↔  ∀ (n : ℕ → ℕ),    StrictMono n →      Filter.Tendsto (fun k => ↑(n (k + 1)) / ↑k.succ) Filter.atTop Filter.atTop →        Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (n k)))
OpenStatement only, no proof