Erdős Problem 587

Reference: erdosproblems.com/587

def Erdos587.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

• Erdos587.MaxNotSqSum N = {A ∈ (Finset.Icc 1 N).powerset | ∀ S ⊆ A, S ≠ ⊥ → ¬IsSquare (∑ n ∈ S, n)}.sup Finset.card

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

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