Ben Green's Open Problem 58

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

theorem Green58.green_58 : sorry ↔ ∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, ∀ B ⊆ Finset.Icc 1 N, ↑N ^ 0.49 ≤ ↑A.card → ↑N ^ 0.49 ≤ ↑B.card → ∃ m ∈ A + B, m.Composite

Suppose $A, B ⊆ \{1, \dots, N\}$ both have size at least $N^{0.49}$. Must the sumset $A + B$ contain a composite number?