---

Claim. The answer to Problem 267 is yes: for every strictly increasing sequence of positive integers $n_1<n_2<\cdots$ for which some real $c>1$ has $n_{k+1}/n_k\ge c$ for all $k$, the sum $\sum_k 1/F_{n_k}$ is irrational. The claim was submitted to the problem's proof-claims thread on 2026-07-15 by Colin Snyder (account coffeewithcolin), who credits the proof to an AI system (GPT 5.6, run in a custom harness) and gives as its write-up a page of the Star Fleet Math site (the preprint link) and as its proof a downloadable Lean 4 bundle (the first formalization link). The thread entry says that the case $c\ge2$ was classical (Badea 1993, the accepted partial claim on the Badea page) and that the open case was $1<c<2$.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

We claim the answer is yes for the full range: for every index sequence with $n_{k+1}/n_k\ge c$ for some real $c>1$, the sum $\sum_k 1/F_{n_k}$ is irrational. Proved in Lean 4 / Mathlib (theorem erdos_problem_267), standard axioms only, no sorry. For $c\ge 2$ this was classical (Badea, 1993); the open case was $1<c<2$. Idea: suppose the total is rational. The identity $1/F_n=\sqrt5\sum_j(-1)^{nj}\varphi^{-(2j+1)n}$ rewrites the series as an integer coefficient word over $\mathbb{Z}[\varphi]$, and rationality pins its residuals to a fixed lattice. Comparing two suitable windows of the word then produces a nonzero element of $\mathbb{Z}[\varphi]$ with norm strictly between $0$ and $1$, which cannot exist. Deep dyadic structure in the indices is deleted exactly first, and a CRT density argument locates the required windows, with an explicit cutoff. Notes: The $c\ge 2$ range is prior art (Badea's criterion); the contribution is the full range $c>1$. Verify: "lake exe cache get", "lake --wfail build", then "#print axioms erdos_problem_267" gives exactly [propext, Classical.choice, Quot.sound]. The bundle includes a line-by-line statement-fidelity audit.

The formal statement. The bundle's pinned target, Research/Basic.lean, defines reciprocalFibSeries n as the real tsum of (Nat.fib (n k))⁻¹ over k, and HasRatioGap n as the existence of a real $c>1$ with $c\le n(k+1)/n(k)$ (real division of the casts) for every $k$; the theorem erdos_problem_267 takes n : ℕ → ℕ with every value positive, StrictMono n and HasRatioGap n, and concludes Irrational (reciprocalFibSeries n). Compared with the site's wording: positivity of the indices keeps Mathlib's Nat.fib (which starts $0,1,1,2,\ldots$) aligned with $F_1=F_2=1$; the gap hypothesis is the problem's $n_{k+1}/n_k\ge c>1$ with $c$ quantified over the reals; summability is not assumed. The proof is a self-contained file of 27,673 lines (Erdos267Standalone.lean, importing only Mathlib), under Lean v4.31.0 with Mathlib pinned at a stable commit in the bundle's manifest. The bundle's own audit note dates its lake --wfail build to 2026-07-12. The formal-conjectures statement file for the problem (the record link, pinned at the repository's commit of 2026-09-18) tags erdos_267 as research solved, with answer yes, and cites as its formal proof a copy of the same Basic.lean in a third repository, pinned above at the commit of 2026-07-30 (the second formalization link); the two pinned files agree line for line. The formal-conjectures statement quantifies $c$ over the rationals, which is equivalent since every real $c>1$ has a rational below it and above $1$.

Argument, as the write-up describes it. Suppose the sum is rational. The identity $1/F_n=\sqrt5\sum_{j\ge0}(-1)^{nj}\varphi^{-(2j+1)n}$ turns the series into an integer-coefficient word over $\mathbb{Z}[\varphi]$ whose normalized residuals a rational total pins to a fixed lattice; comparing two suitably placed windows of that word yields a nonzero element of $\mathbb{Z}[\varphi]$ of norm strictly between $0$ and $1$. Indices with unbounded two-adic order are first removed exactly, as complete dyadic tails whose deletion keeps the ratio gap, and a density argument through the Chinese remainder theorem locates the windows below an explicit cutoff.

Standing. Claimed. The site labels the problem OPEN (page last edited 18 January 2026); as of 2026-10-07 the proof-claim entry has no comments and the curator has not commented on it. The Star Fleet Math page carries a referee report produced by an automated agent, not by a named mathematician; it is the site's own process, not outside acceptance. There is no refereed or arXiv write-up. The corpus records no build of the Lean bundle, no print of its axioms and no audit of its definitions beyond the description above, so the claim carries no formalized evidence and the formalizations are links, not a warrant.

Depends on. Nothing in this wiki.