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

Erdős ProblemsNumber theory

Erdős Problem 267: Generalisation Ratio Limit To Infinity

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 nkk→∞\frac {n_k}{k} \to \infty. 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 nkk→∞\frac {n_k}{k} \to \infty. 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.variants.generalisation_ratio_limit_to_infinity

Canonical source
Complete statement target, proof intentionally absentLean 4
theorem erdos_267.variants.generalisation_ratio_limit_to_infinity : answer(sorry) ↔ ∀ (n : ℕ → ℕ),    StrictMono n → Filter.Tendsto (fun k => (n (k+1) / k.succ : ℝ)) Filter.atTop Filter.atTop →    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