Skip to content

Erdős problem 1

Start work

If A⊆{1,...,N}A\subseteq\{1, ..., N\} with ∣A∣=n|A| = n is such that the subset sums ∑a∈Sa\sum_{a\in S}a are distinct for all S⊆AS\subseteq A then N≫2n. N \gg 2 ^ n.

Sources

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1.lean

Retained formal statement3 of 8

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

FormalConjectures/ErdosProblems/1.leanErdos1.erdos_1.variants.lb_strong3 linesExact file
∃ o,  ∃ (_ : o =o[Filter.atTop] 1),    ∀ (N : ℕ) (A : Finset ℕ), Erdos1.IsSumDistinctSet A N → (√(2 / Real.pi) - o A.card) * 2 ^ A.card / √↑A.card ≤ ↑N
SolvedStatement only, no proof