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.
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/350.leanErdos350.DecidableDistinctSubsetSums {1, 2}TestStatement only, no proof
Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:350 - PLBY Lean proofs
ErdosProblems.Erdos350
Reported activity
Reported by these sources. Not reviewed here.
Formalization
- Machine