erdos_41_i

Specification

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`?

Prize

$500

Paul Erdős

Lean 4 Statement

theorem erdos_41_i (A : Set ℕ) (h_pair : NtupleCondition A 2) (h_infinite : A.Infinite) :
    Filter.atTop.liminf (fun N => (A.interIcc 1 N).ncard / (N : ℝ).sqrt) = 0

ID: ErdosProblems__41__erdos_41_i

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof