Erdős Problem 41

Conjecture 41 · Erdős

Let $A \subset \mathbb{N}$ 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 \to \infty} \frac{\lvert A \cap \{1,\ldots,N\}\rvert}{N^{1/3}}=0?$

Formal statement · Lean 4.lean

theorem erdos_41 (A : Set ℕ) (h_triple : NtupleCondition A 3) (h_infinite : A.Infinite) :
    Filter.atTop.liminf (fun N => (A ∩ Icc 1 N).ncard / (N : ℝ)^(1/3 : ℝ)) = 0 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗