Skip to content

Erdős problem 276

Is there an infinite Lucas sequence a0,a1,a_0, a_1, \ldots where an+2=an+1+ana_{n+2} = a_{n+1} + a_n for n0n \ge 0 such that all aka_k are composite, and yet no integer has a common factor with every term of the sequence?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

276.lean

Retained formal statement1 of 1

Is there an infinite Lucas sequence a0,a1,a_0, a_1, \ldots where an+2=an+1+ana_{n+2} = a_{n+1} + a_n for n0n \ge 0 such that all aka_k are composite, and yet no integer has a common factor with every term of the sequence?

FormalConjectures/ErdosProblems/276.leanErdos276.erdos_2761 lineExact file
True ↔ ∃ a, Erdos276.IsLucasSequence a ∧ (∀ (k : ℕ), (a k).Composite) ∧ ∀ n > 1, ∃ k, n.gcd (a k) = 1
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page