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 ?
∀ (N : ℕ), Erdos321.R N = sorryOpenStatement only, no proofformal statement reference