Skip to content

Erdős problem 267

If n1<n2<⋯n_1 < n_2 < \cdots with nk+1/nk≥c>1n_{k+1}/n_k \ge c > 1, must ∑k1/Fnk\sum_k 1/F_{n_k} be irrational? The proposed proof closes the range 1<c<21 < c < 2 left open by earlier criteria.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/267.lean

Formal Conjectures

FormalConjectures/ErdosProblems/267.leanErdos267.erdos_2673 linesExact file
True ↔  ∀ (n : ℕ → ℕ),    ∀ c > 1, StrictMono n → (∀ (k : ℕ), c ≤ ↑(n (k + 1)) / ↑(n k)) → Irrational (∑' (k : ℕ), 1 / ↑(Nat.fib (n k)))
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • William Blair Lean proofswilliamjblair:Research.erdos_problem_267

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • argument

    VibeMathed

    Machine
    GPT-5.6 starships (Claude Fable 5 reviewer)
    Reported outcome
    candidate
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page