erdos_1.variants.lb

Specification

Erdős and Moser [Er56] proved $$ N \geq (\tfrac{1}{4} - o(1)) \frac{2^n}{\sqrt{n}}. $$ [Er56] Erdős, P., _Problems and results in additive number theory_. Colloque sur la Th\'{E}orie des Nombres, Bruxelles, 1955 (1956), 127-137.

Prize

$500

Paul Erdős

Lean 4 Statement

theorem erdos_1.variants.lb : ∃ (o : ℕ → ℝ) (_ : o =o[atTop] (1 : ℕ → ℝ)),
    ∀ (N : ℕ) (A : Finset ℕ) (h : IsSumDistinctSet A N),
      (1 / 4 - o A.card) * 2 ^ A.card / (A.card : ℝ).sqrt ≤ N

ID: ErdosProblems__1__erdos_1.variants.lb

Actions

Submit a Proof

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

Submit Proof