Sets with no element dividing a product of two others

DefinitionSets in which no element divides the product of two others#✓fully proved

A finite set \(A\) of natural numbers is good when every element of \(A\) is positive and no \(a \in A\) divides \(bc\) for any \(b, c \in A\) with \(a \ne b\) and \(a \ne c\); here \(b = c\) is allowed.

def Good (A : Finset ℕ) : Prop :=
  (∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a ≠ b → a ≠ c → ¬ a ∣ b * c) ∧ (∀ a ∈ A, 1 ≤ a)

Used by 1

Used byMaximum size of a good subset

DefinitionMaximum size of a good subset#✓fully proved

For a natural number \(n\), \(F(n)\) is the largest size of a good subset of \(\{1, \dots, n\}\), defined as the supremum of the sizes of the good sets \(A \subseteq \{1, \dots, n\}\).

noncomputable def F (n : ℕ) : ℕ :=
  sSup {k | ∃ A : Finset ℕ, A ⊆ Finset.Icc 1 n ∧ Good A ∧ A.card = k}

Uses 1 · Used by 1

Statement usesSets in which no element divides the product of two others

Used byStatement of Erdős Problem 793

DefinitionStatement of Erdős Problem 793#✓fully proved

For a natural number \(n\), let \(F(n)\) be the largest size of a set \(A \subseteq \{1, \dots, n\}\) with \(a \nmid bc\) for all \(a, b, c \in A\) such that \(a \ne b\) and \(a \ne c\), and let \(\pi(n)\) be the number of primes at most \(n\). This is the proposition that there is a real constant \(C > 0\) such that \((F(n) - \pi(n)) / (n^{2/3} / (\log n)^2) \to C\) as \(n \to \infty\). Equivalently, \(F(n) = \pi(n) + (C + o(1))\, n^{2/3} / (\log n)^2\).

def conjecture : Prop :=
  ∃ C : ℝ, 0 < C ∧ Filter.Tendsto
    (fun n : ℕ => (((F n : ℤ) - (Nat.primeCounting n : ℤ)) : ℝ) /
      ((n : ℝ) ^ ((2 : ℝ) / 3) / (Real.log n) ^ 2))
    Filter.atTop (nhds C)

Uses 1 · Used by 1

Statement usesMaximum size of a good subset

Used byErdős Problem 793 has a positive answer

TheoremErdős Problem 793 has a positive answer#●ready to prove

Let \(F(n)\) be the largest size of a set \(A \subseteq \{1, \dots, n\}\) such that \(a \nmid bc\) whenever \(a, b, c \in A\) with \(a \ne b\) and \(a \ne c\) (\(b = c\) is allowed), and let \(\pi(n)\) be the number of primes at most \(n\). Then there is a real constant \(C > 0\) such that \((F(n) - \pi(n)) / (n^{2/3} / (\log n)^2) \to C\) as \(n \to \infty\).

Chojecki (2026, Theorem 1.1) proves this with \(C = 27/2\).

public theorem_wanted conjecture_holds : conjecture

Sources

• P. Chojecki, The Second Term for Strongly 2-Primitive Sets, arXiv preprint (2026), arXiv:2607.15306, https://arxiv.org/abs/2607.15306.

Uses 1

Statement usesStatement of Erdős Problem 793

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.