Erdős Problem #326

Does there exist \(A = \{a_1 < a_2 < \cdots\} \subset \mathbb{N}\) which is a minimal basis of order \(2\) (i.e. every large integer is the sum of \(2\) elements from \(A\), and no proper subset of \(A\) has this property), such that \[\lim_{k\to\infty} \frac{a_k}{k^2} = c\] for some \(c \neq 0\)? Erdős and Graham conjectured a negative answer to this question [ErGr80]. "Minimal basis of order \(2\)" is formalised as `Minimal` for the predicate `Set.IsAsymptoticAddBasisOfOrder · 2` on sets of naturals ordered by inclusion.