The board / irrationality / #267
Erdős Problem #267
OPENdatabase updated 2025-08-31
No proof or disproof is known, and it isn't known whether a finite computation could settle it.
What the community database records, not our verdict. erdosproblems.com no longer shows statuses (why).
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?
Statement as formalized in Formal Conjectures (Google DeepMind, Apache-2.0) · their label: research solved · 3 further variants / known partial results in the Lean file. The authoritative wording is on erdosproblems.com/267.Prizenone
Topicsirrationality
Statement in LeanFormal Conjectures
Solution in Leanno
Original pageerdosproblems.com/267
Attempts
submit one →Read our working report →
Live page status OPEN, but it lists one full proof claim (Colin Snyder, submitted 2026-07-15, claiming the complete \(c>1\) result with a Lean 4/Mathlib formalisation); currently working and intereste
SKIPPED