Erdős Problem 943

Reference: erdosproblems.com/943

theorem Erdos943.erdos_943 : (∃ (o : ℕ → ℝ), o =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(AdditiveCombinatorics.sumRep Nat.Powerful n) = ↑n ^ o n) ↔ sorry

Let $A$ be the set of powerful numbers. Is is true that $1_A\ast 1_A(n)=n^{o(1)}$ for every $n$?