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

Good [Go74] and Bicknell and Hoggatt [BiHo76] have shown that $\sum_n \frac 1 {F_{2^n}}$ is irrational.

Formal proof provided by AlphaProof Ref: * [Go74] Good, I. J., _A reciprocal series of Fibonacci numbers_ * [BiHo76] Hoggatt, Jr., V. E. and Bicknell, Marjorie, _A reciprocal series of Fibonacci numbers with subscripts $2\sp{n}k$ _

FormalConjectures/ErdosProblems/267.leanErdos267.erdos_267.variants.specialization_pow_two1 lineExact file

1Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (2 ^ k)))

SolvedProof has a holeformal conjecturesexternal proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science