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
Erdos350.DecidableDistinctSubsetSums {1, 2}TestStatement only, no proof