Erdős problem 587

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

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