Erdős problem 350
If A ⊂ ℕ is a finite set of integers all of whose subset sums are distinct then ∑ n ∈ A, 1/n < 2. Proved by Ryavec.
Sources
FormalConjectures/ErdosProblems/
350.lean
Retained formal statement
If A ⊂ ℕ is a finite set of integers all of whose subset sums are distinct then ∑ n ∈ A, 1/n^s < 1/(1 - 2^(-s)), for any s > 0. Proved by Hanson, Steele, and Stenger [HSS77].
We exclude here the case s = 0, because in the informal formulation then the right hand side is to be interpreted as ∞, while the left hand side counts the elements in A.
∀ (A : Finset ℕ), Erdos350.DecidableDistinctSubsetSums A → ∀ (s : ℝ), 0 < s → ∑ n ∈ A, (1 / ↑n) ^ s < 1 / (1 - 2 ^ (-s))SolvedStatement only, no proof