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 statement2 of 4

The sum ∑n1Fn\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_.

FormalConjectures/ErdosProblems/267.leanErdos267.erdos_267.variants.fibonacci_inverse_sum1 lineExact file
Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib k))
SolvedStatement only, no proof