Erdős Problem 477

Reference: erdosproblems.com/477

theorem erdos_477 : (∀ (f : Polynomial ℤ), 2 ≤ f.degree → ∃ (A : Set ℤ), ∀ (z : ℤ), ∃! a : ℤ × ℤ, (a ∈ A ×ˢ Set.range fun (a : ℤ) => Polynomial.eval a f) ∧ z = a.1 + a.2) ↔ sorry

Let $f: \mathbb{Z} \rightarrow \mathbb{Z}$ be a polynomial of degree at least $2$.

Is there a set $A$ such that every $z \in \mathbb{Z}$ has exactly one representation as $z = a + f(n)$ for some $a \in A$ and $n \in \mathbb{Z}$?

theorem erdos_477.variants.strong_negation (f : Polynomial ℤ) (hf₀ : 2 ≤ f.degree) : ¬∃ (A : Set ℤ), ∀ (z : ℤ), ∃! a : ℤ × ℤ, (a ∈ A ×ˢ Set.range fun (a : ℤ) => Polynomial.eval a f) ∧ z = a.1 + a.2

Probably there is no such $A$ for any polynomial $f$.