Formal target: Corpus.Erdos359.erdos_359.parts.i

Let $a_1< a_2 < ⋯ $ be an infinite sequence of integers such that $a_1=1$ and $a_{i+1}$ is the least integer which is not a sum of consecutive earlier $a_j$s.

Exact formal statement

∀ (A : Nat → Nat),
  Corpus.Erdos359.IsGoodFor A 1 →
    Filter.Tendsto.{0, 0} (fun k => HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (A k)) (Nat.cast.{0} k)) Filter.atTop.{0}
      Filter.atTop.{0}

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record