Formal target: Corpus.Erdos539.erdos_539.variants.sq

Let $h(n)$ be maximal such that, for any set $A\subseteq \mathbb{N}$ of size $n$, the set$$\left\{ \frac{a}{(a,b)}: a,b\in A\right\}$$has size at least $h(n)$.

Exact formal statement

Asymptotics.IsTheta.{0, 0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (Corpus.Erdos539.cofactorThreshold n)) fun n =>
  (Nat.cast.{0} n).sqrt

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record