Erdős problem 1

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

Sources

The source's own material, retained exactly.

8 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1.lean

Retained formal statement1 of 8

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

FormalConjectures/ErdosProblems/1.leanErdos1.erdos_11 lineExact file

1∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), Erdos1.IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N

OpenStatement only, no proof