Erdős Problem 587

Reference: erdosproblems.com/587

def MaxNotSqSum (N : ℕ) : ℕ

MaxNotSqSum N is the size of the largest subset A of {1,...,N} such that for all non-empty S ⊆ A, the sum ∑ n ∈ S, n is not a square.

Equations

• MaxNotSqSum N = (Finset.filter (fun (A : Finset ℕ) => ∀ S ⊆ A, S ≠ ⊥ → ¬IsSquare (∑ n ∈ S, n)) (Finset.Icc 1 N).powerset).sup Finset.card

theorem erdos_587.variants.nguyen_vu : ∃ O > 0, ∃ O' > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(MaxNotSqSum N) ≤ O' * ↑N ^ (1 / 3) * Real.log ↑N ^ O

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