Claim in Erdős problems that formal-conjectures marks solved

A published paper or arXiv preprint answers the main question of Erdős Problem #267 (theorem erdos_267 in formal-conjectures) in full (proof, disproof, or the exact value asked for) with no hypotheses beyond the problem's own.

Problem as stated at github.com/google-deepmind/formal-conjectures/blob/34ee0e3c5fd52d202d62a71094a37970cb5fb870/FormalConjectures/ErdosProblems/267.lean. The claim text is written by Corroborate; that site has not reviewed or endorsed it.

The problem, as stated in formal-conjectures (Apache 2.0):

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?

Verdict: no verdict yet

formal-conjectures marks problem #267 as solved. Those pages say who settled it and how.

Evidence for

None yet.

Evidence against

None yet.