Erdős Problem 341

Reference: erdosproblems.com/341

theorem Erdos341.erdos_341 : sorry ↔ ∀ (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 m

Let $A=\{a_1 < \cdots < a_k\}$ be a finite set of integers and extend it to an infinite sequence $\overline{A}=\{a_1 < a_2 < \cdots \}$ by defining $a_{n+1}$ for $n \geq k$ to be the least integer exceeding $a_n$ which is not of the form $a_i + a_j$ with $i,j \leq n$. Is it true that the sequence of differences $a_{m+1}-a_m$ is eventually periodic?

This problem is discussed under Problem 7 on Green's open problems list.