Formal target: Corpus.Erdos357.erdos_357.parts.i

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.

Exact formal statement

Asymptotics.IsLittleO.{0, 0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (Corpus.Erdos357.f n)) fun n => Nat.cast.{0} n

This target is a formal statement, not a proof of the problem.

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record