Erdős problem 357
Let be the maximal such that there exist integers such that all sums of the shape are distinct. It is known that . Source: See comment by Desmond Weisenberg here: https://www.erdosproblems.com/forum/thread/357.
Sources
FormalConjectures/ErdosProblems/
357.lean
Retained formal statement
Let be the maximal such that there exist integers such that all sums of the shape are distinct. How does grow? Can we find a (good) explicit function such that ?
(fun n => ↑(Erdos357.f n)) =Θ[Filter.atTop] sorryOpenStatement only, no proof