Erdős problem 789

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

Sources

The source's own material, retained exactly.

7 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

789.lean

Retained formal statement3 of 7

Erdős [Er62c] and Choi [Ch74b] proved that $(n\log(n))^{1/3}\ll h(n)$ .

FormalConjectures/ErdosProblems/789.leanErdos789.erdos_789.variants.cube_root_linearithmic_isBigO1 lineExact file

1(fun n => (↑n * Real.log ↑n) ^ (1 / 3)) =O[Filter.atTop] fun n => ↑(Erdos789.subsetSumThreshold n)

SolvedStatement only, no proof