Erdős Problem 749

Reference: erdosproblems.com/749

theorem Erdos749.erdos_749 : sorry ↔ ∀ ε > 0, ∃ (A : Set ℕ), 1 - ε ≤ (A + A).lowerDensity ∧ (Nat.cast ∘ AdditiveCombinatorics.sumRep A) =O[Filter.atTop] fun (n : ℕ) => 1

Let $\epsilon>0$. Does there exist $A\subseteq \mathbb{N}$ such that the lower density of $A+A$ is at least $1-\epsilon$ and yet $1_A\ast 1_A(n) \ll_\epsilon 1$ for all $n$?