---
id: F-192
title: Faithful formal solution of Erdős Problem 267
tier: lean
polarity: positive
depends_on: [F-191]
supersedes: []
verifier: cd workspace/shared/lean_mathlib && lake env lean -E warning ../../../verified_math/F-192_erdos-267-faithful-theorem/Erdos267Standalone.lean
date: 2026-07-12
---

## Statement

With

`reciprocalFibSeries n = ∑' k, (Nat.fib (n k) : ℝ)⁻¹`

and

`HasRatioGap n = ∃ c : ℝ, 1<c ∧ ∀k, c≤(n(k+1):ℝ)/(n k:ℝ)`,

`erdos_problem_267` proves that every positive strictly increasing `n : ℕ → ℕ` satisfying `HasRatioGap n` has `Irrational (reciprocalFibSeries n)`.

This is the line-by-line faithful formalization audited in `check_answer/README.md`.

## Proof / verification

Extract the uniform `c>1`. Positivity of `n_k` converts the quotient inequality exactly to `c·n_k≤n_{k+1}`. Apply F-191, which rules out rationality by finite complete-dyadic-tail deletion followed by the bounded-order reverse-window contradiction.

`Erdos267Standalone.lean` contains the full dependency closure and faithful wrapper in one warning-free artifact. `Basic.lean` is the exact pinned target source. Independently, the project verifier command `cd workspace/experiments/experiment_1_pin_statement/lean && lake --wfail build` also succeeds.
