therefore
Sign up
Open navigation
All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsNumber theory

Erdős Problem 267

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 nk+1nk≥c>1\frac{n_{k+1}}{n_k} \ge c > 1. Must ∑k1Fnk\sum_k \frac 1 {F_{n_k}} be irrational?

Number theoryAMS 11

Mathematical statement

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 nk+1nk≥c>1\frac{n_{k+1}}{n_k} \ge c > 1. Must ∑k1Fnk\sum_k \frac 1 {F_{n_k}} be irrational?

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_267

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_267 : answer(sorry) ↔ ∀ᵉ (n : ℕ → ℕ) (c > (1 : ℚ)), StrictMono n → (∀ k, c ≤ n (k+1) / n k) →    Irrational (∑' k, 1 / (Nat.fib <| n k)) := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References

Pinned Formal Conjectures sourceformalizationerdosproblems.com/267background