---

Claim. $\sum_{k\ge0}1/F_{2^k}$ is irrational, so the instance $n_k=2^k$ of Problem 267 has answer yes. The proof is the theorem erdos_267.variants.specialization_pow_two in a fork of the formal-conjectures repository, at the commit of 24 April 2026 linked first above, stated for Mathlib's Nat.fib and proved without sorry inside the statement file. The formal-conjectures statement file for the problem (the record link) tags the variant research solved, cites that proof in its formal_proof attribute and says that the formal proof was provided by AlphaProof; the attribute entered the file on 24 April 2026. The argument is AlphaProof's own tail-and-denominator estimate, not the telescoping identity of Good's evaluation.

Covers. The instance $n_k=2^k$: the answer is yes. Not covered: every other index sequence. The instance lies inside Badea's 1993 condition (the Badea page), and Good's 1974 evaluation of the sum as $(7-\sqrt5)/2$ (the Good page) settled it first.

Depends on. No page of this wiki.

Acceptance. None recorded. The site labels the problem OPEN and its commentary does not mention the proof; this corpus has not built the proof or audited its statement, so the links are not formalized evidence. The proof is attributed to AlphaProof, as the statement file names it.