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. It is known that
∃ o o', o =o[Filter.atTop] 1 ∧ o' =o[Filter.atTop] 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos357.g n) ∈ Set.Icc ((1 / 3 + o n) * ↑n) ((2 / 3 + o' n) * ↑n)OpenStatement only, no proof