Erdős problem 789 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

789.lean

Retained formal statement4 of 7

By the solved variant erdos_789.variants.cube_root_linearithmic_isBigO, in order to prove erdos_789.variants.cube_root_linarithmic it suffices to show $h(n) = O((n\log(n))^{1/3})$ .

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

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

OpenStatement only, no proof

Sources

Search problems.science