Formal target: Corpus.Erdos1.erdos_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.

Exact formal statement

Exists.{1} fun C =>
  And (GT.gt.{0} C 0)
    (∀ (N : Nat) (A : Finset.{0} Nat),
      Corpus.Erdos1.IsSumDistinctSet A N →
        Ne.{1} N 0 → LT.lt.{0} (HMul.hMul.{0, 0, 0} C (HPow.hPow.{0, 0, 0} 2 (Finset.card.{0} A))) (Nat.cast.{0} N))

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record