Erdős problem 276
Is there an infinite Lucas sequence where for such that all are composite, and yet no integer has a common factor with every term of the sequence?
Sources
FormalConjectures/ErdosProblems/
276.lean
Retained formal statement
Is there an infinite Lucas sequence where for such that all are composite, and yet no integer has a common factor with every term of the sequence?
True ↔ ∃ a, Erdos276.IsLucasSequence a ∧ (∀ (k : ℕ), (a k).Composite) ∧ ∀ n > 1, ∃ k, n.gcd (a k) = 1OpenStatement only, no proof