If $A \subset N$ is a finite set of integers which is dissociated (that is, all of the subset sums are distinct) then $n \in A \sum \frac{1}{n} < 2.$

Worked, still open.

number theory · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 5 11 · test (literature)

theorem decidableDistinctSubsetSums_1_2 : DecidableDistinctSubsetSums {1, 2}

solved