Erdős Problem 1196

Reference: erdosproblems.com/1196

def Erdos1196.IsPrimitive {M : Type u_1} [CommMonoid M] (A : Set M) : Prop

A set is primitive if no non-associated elements of the set divide each other.

Equations

• Erdos1196.IsPrimitive A = ∀ x ∈ A, ∀ y ∈ A, x ∣ y → Associated x y

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

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$?