Skip to content

Erdős problem 350

Start work

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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

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
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (A : Finset M),  Erdos350.DistinctSubsetSums ↑A ↔ Erdos350.DecidableDistinctSubsetSums A
APIStatement only, no proof