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 maximal such size. Results of Bleicher and Erdős from [BlEr75] and [BlEr76b] imply that valid for any with and any with . (In these bounds denotes the -fold iterated logarithm.)
[BlEr75] Bleicher, M. N. and Erdős, P., _The number of distinct subsums of _. Math. Comp. (1975), 29-42. [BlEr76b] Bleicher, Michael N. and Erdős, Paul, _Denominators of Egyptian fractions. II_. Illinois J. Math. (1976), 598-613.
∀ (N k : ℕ), 4 ≤ k → ↑k ≤ Real.log^[k] ↑N → ↑N / Real.log ↑N * ∏ i ∈ Finset.Icc 3 k, Real.log^[i] ↑N ≤ ↑(Erdos321.R N)SolvedStatement only, no proofformal statement reference