Erdős problem 267 · problems.science

If $n_1 < n_2 < \cdots$ with $n_{k+1}/n_k \ge c > 1$ , must $\sum_k 1/F_{n_k}$ be irrational? The proposed proof closes the range $1 < c < 2$ left open by earlier criteria.

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

267.lean

Retained formal statement3 of 4

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?

FormalConjectures/ErdosProblems/267.leanErdos267.erdos_267.variants.generalisation_ratio_limit_to_infinity5 linesExact file

1True ↔2  ∀ (n : ℕ → ℕ),3    StrictMono n →4      Filter.Tendsto (fun k => ↑(n (k + 1)) / ↑k.succ) Filter.atTop Filter.atTop →5        Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (n k)))

OpenStatement only, no proof

Sources

Search problems.science