Erdős problem 442

Tao resolved erdos_442 in the negative in Theorem 1 of https://arxiv.org/pdf/2407.04226. The following is a formalisation of that theorem with $C_0 = 1$.

Let $\operatorname{Log} x := \max\{\log x, 1\}$, $\operatorname{Log}_2x = \operatorname{Log} (\operatorname{Log} x)$, and $\operatorname{Log}_3x = \operatorname{Log}(\operatorname{Log}(\operatorname{Log} x)).$ There exists a set $A$ of natural numbers such that $$\sum_{n\in A: n\leq x} \frac{1}{n} = \exp\left(\left(\left(\frac{1}{2} + o(1)\right)\operatorname{Log}_2^{1/2}x \operatorname{Log}_3x\right)\right)$$ and $$\sum_{n, m\in A: n, m\leq x} \frac{1}{\operatorname{lcm}(n, m)}\ll\left(\sum_{n\in A: n\leq x} \frac{1}{n}\right)^2$$