Erdős problem 587 · problems.science

Nguyen and Vu proved that $|A| \ll N^{1/3} (\log N)^{O(1)}$ .

Sources

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

1 retained statement2415f78e850a

FormalConjectures/ErdosProblems/

587.lean

Retained formal statement1 of 1

Nguyen and Vu proved that $|A| \ll N^{1/3} (\log N)^{O(1)}$ .

FormalConjectures/ErdosProblems/587.leanErdos587.erdos_587.variants.nguyen_vu1 lineExact file

1∃ O > 0, ∃ O' > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos587.MaxNotSqSum N) ≤ O' * Real.nthRoot 3 ↑N * Real.log ↑N ^ O

SolvedStatement only, no proof