Formal target: Corpus.Erdos789.erdos_789.variants.sq

Let $h(n)$ be maximal such that if $A\subseteq \mathbb{Z}$ with $\lvert A\rvert=n$ then there is $B\subseteq A$ with $\lvert B\rvert \geq h(n)$ such that if $a_1+\cdots+a_r=b_1+\cdots+b_s$ with $a_i,b_i\in B$ then $r=s$.

Exact formal statement

Asymptotics.IsTheta.{0, 0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (Corpus.Erdos789.subsetSumThreshold 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