Erdős problem 41
Let A ⊆ ℕ be an infinite set such that the triple sums a + b + c are all distinct for a, b, c in A (aside from the trivial coincidences). Is it true that liminf n → ∞ |A ∩ {1, …, N}| / N^(1/3) = 0?
Sources
FormalConjectures/ErdosProblems/
41.lean
Retained formal statement
Erdős proved the following pairwise version. Let A ⊆ ℕ be an infinite set such that the pairwise sums a + b are all distinct for a, b in A (aside from the trivial coincidences). Is it true that liminf n → ∞ |A ∩ {1, …, N}| / N^(1/2) = 0?
∀ (A : Set ℕ), Erdos41.NtupleCondition A 2 → A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / √↑N) Filter.atTop = 0SolvedStatement only, no proof