Erdős Problem 326

Reference: erdosproblems.com/326

theorem erdos_326 : (∀ (A : Set ℕ), A.IsAddBasisOfOrder 2 → ∃ (b : ℕ → ℕ), StrictMono b ∧ ∀ (n : ℕ), b n ∈ A ∧ (Set.range b).IsAddBasis ∧ ∀ (x : ℝ), ¬Filter.Tendsto (fun (n : ℕ) => ↑(b n) / ↑n ^ 2) Filter.atTop (nhds x)) ↔ sorry

Let $A \subset \mathbb{N}$ be an additive basis of order 2.

Must there exist $B = \{b_1 < b_2 < \dots\} \subseteq A$ which is also a basis such that $\lim_{k\to\infty} \frac{b_k}{k^2}$ does not exist?

theorem erdos_326.variants.eq : (∀ (A : Set ℕ), A.IsAddBasisOfOrder 2 → ∃ (a : ℕ → ℕ), StrictMono a ∧ Set.range a = A ∧ ∀ (x : ℝ), ¬Filter.Tendsto (fun (n : ℕ) => ↑(a n) / ↑n ^ 2) Filter.atTop (nhds x)) ↔ False

Erdős originally asked whether this was true with A = B, but this was disproved by Cassels.