Quotients a/gcd(a, b) in sets of integers

DefinitionCofactor lower bound#✓fully proved

For natural numbers \(n\) and \(m\), \(m\) is a cofactor lower bound for \(n\) when, for every set \(A\) of exactly \(n\) positive integers, the set \(\{a/\gcd(a,b) : a, b \in A\}\) has at least \(m\) elements.

Members of \(A\) are required to be positive since the quotient \(a/\gcd(a,b)\) is undefined at \(a = b = 0\).

def IsCofactorLowerBound (n m : ℕ) : Prop := ∀ A : Finset ℕ, A.card = n →
  (∀ a ∈ A, 0 < a) →
  m ≤ ((A ×ˢ A).image fun (a, b) ↦ a / a.gcd b).card

Used by 1

Used byErdős cofactor threshold

DefinitionErdős cofactor threshold#✓fully proved

For a natural number \(n\), the cofactor threshold \(h(n)\) is the largest natural number \(m\) such that for every set \(A\) of exactly \(n\) positive integers, the set \(\{a/\gcd(a,b) : a, b \in A\}\) has at least \(m\) elements.

noncomputable def cofactorThreshold (n : ℕ) : ℕ :=
  sSup {m | IsCofactorLowerBound n m}

Uses 1 · Used by 1

Statement usesCofactor lower bound

Used byStatement of Erdős Problem 539

DefinitionStatement of Erdős Problem 539#✓fully proved

Let \(h(n)\) denote the cofactor threshold of \(n\). The statement is that \(\sqrt{n} = O(h(n))\) as \(n \to \infty\), that is, there are a real constant \(C\) and an \(n_0\) such that \(\sqrt{n} \le C\,h(n)\) for all natural numbers \(n \ge n_0\).

def conjecture : Prop :=
  (fun n : ℕ ↦ Real.sqrt (n : ℝ)) =O[atTop]
    fun n ↦ (cofactorThreshold n : ℝ)

Uses 1 · Used by 1

Statement usesErdős cofactor threshold

Used byErdős Problem 539: square-root lower bound for the cofactor threshold

TheoremErdős Problem 539: square-root lower bound for the cofactor threshold#●ready to prove

For a natural number \(n\), let \(h(n)\) be the largest natural number \(m\) such that for every set \(A\) of exactly \(n\) positive integers, the set \(\{a/\gcd(a,b) : a, b \in A\}\) has at least \(m\) elements. Then \(\sqrt{n} = O(h(n))\) as \(n \to \infty\): there are a real constant \(C\) and an \(n_0\) such that \(\sqrt{n} \le C\,h(n)\) for all natural numbers \(n \ge n_0\).

This lower bound was proved by Erdős and Szemerédi. The open problem of determining the exact order of growth of \(h(n)\) is not part of this statement.

public theorem_wanted conjecture_holds : conjecture

Sources

• J. Schmitt, T. Gehrunger, J. Dekoninck, G. Bérczi, U. Kreitner, L. Price, D. Holmes, ProofCouncil: An LLM Agent for Solving Open Mathematical Problems, arXiv:2607.09474 (2026), https://arxiv.org/abs/2607.09474.

Uses 1

Statement usesStatement of Erdős Problem 539

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.