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 statement1 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+1}}{n_k} \ge c > 1$ . Must $\sum_k \frac 1 {F_{n_k}}$ be irrational?

FormalConjectures/ErdosProblems/267.leanErdos267.erdos_2673 linesExact file

1True ↔2  ∀ (n : ℕ → ℕ),3    ∀ c > 1, StrictMono n → (∀ (k : ℕ), c ≤ ↑(n (k + 1)) / ↑(n k)) → Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (n k)))

SolvedProof has a holelean4external 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