Is it true that, for any $x$, if $A\subset [x,\infty )$ is a primitive set of integers (so that no distinct elements of $A$ divide each other) then$$\sum _{a\in A}\frac{1}{a\log a}<1+o(1),$$where the $o(1)$ term $\to 0$ as $x\to \infty$?

AMS 11 · solved (literature)

theorem erdos_1196 :
    answer(True) ↔ ∃ o : ℕ → ℝ, o =o[Filter.atTop] (1 : ℕ → ℝ) ∧ ∀ x > (0 : ℕ), ∀ A ⊆ Set.Ici x, IsPrimitive A →
       ∑' (a : A), (1 / ((a.val : ℝ).log * a)) < 1 + o x