Erdős problem 350 · problems.science

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

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

350.lean

Retained formal statement3 of 5

Small sanity check: the two predicates are saying the same thing.

FormalConjectures/ErdosProblems/350.leanErdos350.DistinctSubsetSums_iff_DecidableDistinctSubsetSums2 linesExact file

1∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (A : Finset M),2  Erdos350.DistinctSubsetSums ↑A ↔ Erdos350.DecidableDistinctSubsetSums A

APIStatement only, no proof

Sources

Search problems.science