Ben Green's Open Problem 63

Let $A$ be the smallest set containing $2$ and $3$ and such that $a_1a_2 - 1 \in A$ if $a_1, a_2 \in A$. Does $A$ have positive density?

References:

• Ben Green's Open Problem 63
• erdosproblems.com/424

This file points to the canonical formalization in FormalConjectures.ErdosProblems.«424».