Erdős Problem 324

Reference: erdosproblems.com/324

theorem Erdos324.erdos_324 : (∃ (f : Polynomial ℤ), Set.InjOn (fun (x : ℕ × ℕ) => match x with | (a, b) => Polynomial.eval (↑a) f + Polynomial.eval (↑b) f) {(a, b) : ℕ × ℕ | a < b}) ↔ sorry

Does there exist a polynomial $f(x)\in\mathbb{Z}[x]$ such that all the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct?

theorem Erdos324.erdos_324.variant.quintic : Set.InjOn (fun (x : ℕ × ℕ) => match x with | (a, b) => a ^ 5 + b ^ 5) {(a, b) : ℕ × ℕ | a < b}

Probably $f(x) = x^5$ has the property that the sums $f(a)+f(b)$ with $a < b$ nonnegative integers are distinct.