Ben Green's Open Problem 61

Reference: [Ben Green's Open Problem 61](https://people.maths.ox.ac.uk/greenbj/papers/open-problems.pdf#section.8 Problem 61)

This problem was originally considered by Erdős and Newman.

theorem Green61.green_61 : sorry ↔ ∃ (f : ℕ → ℝ), Filter.Tendsto f Filter.atTop (nhds 0) ∧ ∀ n ≥ 1, ∀ (A : Finset ℕ), Finset.image (fun (x : ℕ) => x ^ 2) (Finset.Icc 1 n) ⊆ A + A → ↑n ^ (1 - f n) ≤ ↑A.card

Suppose that $A + A$ contains the first $n$ squares. Is $|A| \geq n^{1 - o(1)}$?

It is known that necessarily $|A| \geq n^{2/3 - o(1)}$, whilst in the other direction there do exist such $A$ with $|A| \ll_C n / \log^C n$ for any $C$.