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 $n_{k + 1} / n_{k} \geq c > 1$ . Must $k \sum \frac{1}{F _{n_{k}}}$ be irrational?

Open problem — our best result is machine-sealed: partial proof, reproduced by an independent verifier. The conjecture itself is unsettled.

irrationality · open · formalized (Lean) · 3 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

honest null

needs verification

attempted via frontier '?' (transfer_strength=n/a) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'n/a'. Do not re-attack cold; needs a new idea or richer accumulated context.

partial proof

needs verification

erdos_267 (Fibonacci reciprocal irrationality): the strong form holds for ALL c>=2 (not just c>2) via Badea's criterion (Glasgow Math J 1987) — a KNOWN theorem applied. Formalizable, not novel.

Badea's irrationality criterion for sum 1/a_k with a_{k+1} >= a_k^2 - a_k + 1; applies to the lacunary Fibonacci indices. Result is the known answer, cleanly justified.

Opus cross-check; Badea 1987 cited.

partial proof

machine-sealed

Erdos #267: lean/Vela/Erdos267.lean formalizes the reduction from eventual ratio c >= 2 to Badea's eventual growth condition and, assuming Badea 1993 Corollary 3.2 as a published theorem input, derives the known c >= 2 Fibonacci reciprocal-subseries territory; this does not address the open 1 < c < 2 range.

{"lean_file":"lean/Vela/Erdos267.lean","imported_by":"lean/Vela.lean","formalized_items":["FibonacciReciprocalSubseries using Nat.fib and an infinite Real tsum","BadeaGrowth: eventually 2*n(k)-1 <=...

depends on (the wall): lean/Vela/Erdos267.lean; lean/Vela.lean

[{"method":"lean_kernel","command":"cd lean && lake build Vela.Erdos267","result":"passed"},{"method":"axiom_sorry_scan","command":"rg -n \"sorry|axiom|unsafe|admit\" lean/Vela/Erdos267.lean lean/V...

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is an Erdős–Graham problem (1980), and as stated with only the hypothesis (\displaystyle \frac{n_{k+1}}{n_k}\ge c>1), it is **not known in full generality**.

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_267 : answer(sorry) ↔ ∀ᵉ (n : ℕ → ℕ) (c > (1 : ℚ)), StrictMono n → (∀ k, c ≤ n (k+1) / n k) →
    Irrational (∑' k, 1 / (Nat.fib <| n k))

formal-conjectures/267.lean ↗

Vela formalization: Erdos267.lean (sorry-free)

status

open

evidence

formal

status

Search Vela