Erdős problem 357

Let $f(n)$ be the maximal $k$ such that there exist integers $1 \le a_1 < \dotsc < a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. It is known that $f(n) \geq (2+o(1))\sqrt{n}$ . Source: See comment by Desmond Weisenberg here: https://www.erdosproblems.com/forum/thread/357.

Sources

The source's own material, retained exactly.

17 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

357.lean

Retained formal statement7 of 17

Let $g(n)$ be the maximal $k$ such that there exist integers $1 \le a_1, \dotsc, a_k \le n$ such that all sums of the shape $\sum_{u \le i \le v} a_i$ are distinct. It is known that $\left(\frac 1 3 + o(1) \right)n \leq g(n) \leq \left(\frac 2 3 + o(1) \right)n.$

FormalConjectures/ErdosProblems/357.leanErdos357.erdos_357.variants.hegyvari4 linesExact file

1∃ o o',2  o =o[Filter.atTop] 1 ∧3    o' =o[Filter.atTop] 1 ∧4      ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Erdos357.g n) ∈ Set.Icc ((1 / 3 + o n) * ↑n) ((2 / 3 + o' n) * ↑n)

OpenStatement only, no proof