Erdős problem 321
What is the largest such that all subset sums (over ) are distinct?
Sources
FormalConjectures/ErdosProblems/
321.lean
Retained formal statement
Let be the size of the largest such that all sums are distinct for . What is ?
(fun N => ↑(Erdos321.R N)) =Θ[Filter.atTop] sorryOpenStatement only, no proofformal statement reference