erdos_1.variants.lb_strong

Specification

A number of improvements of the constant $\frac{1}{4}$ have been given, with the current record $\sqrt{2 / \pi}$ first provied in unpublished work of Elkies and Gleason.

Prize

$500

Paul Erdős

Lean 4 Statement

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

ID: ErdosProblems__1__erdos_1.variants.lb_strong

Actions

Submit a Proof

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

Submit Proof