Erdős problem 341
Let be a finite set of integers and extend it to an infinite sequence by defining for to be the least integer exceeding which is not of the form with . Is it true that the sequence of differences is eventually periodic?
Sources
FormalConjectures/ErdosProblems/
341.lean
Retained formal statement
Let be a finite set of integers and extend it to an infinite sequence by defining for to be the least integer exceeding which is not of the form with . Is it true that the sequence of differences is eventually periodic?
This problem is discussed under Problem 7 on Green's open problems list.
True ↔ ∀ (a : ℕ → ℤ), (∀ᶠ (n : ℕ) in Filter.atTop, IsLeast {x | a n < x ∧ x ∉ {x | ∃ i ≤ n, ∃ j ≤ n, a i + a j = x}} (a (n + 1))) → have d := fun i => a (i + 1) - a i; ∃ p > 0, ∀ᶠ (m : ℕ) in Filter.atTop, d (m + p) = d mOpenStatement only, no proof