Formal target: Corpus.Erdos208.erdos_208.variants.log_bound

In [Er79] Erdős says perhaps $s_{n+1} - s_n \ll \log s_n$, but he is 'very doubtful'.

Exact formal statement

Asymptotics.IsBigO.{0, 0, 0} Filter.atTop.{0}
  (fun n =>
    HSub.hSub.{0, 0, 0} (Nat.cast.{0} (Corpus.Erdos208.erdos208.s (HAdd.hAdd.{0, 0, 0} n 1)))
      (Nat.cast.{0} (Corpus.Erdos208.erdos208.s n)))
  fun n => Real.log (Nat.cast.{0} (Corpus.Erdos208.erdos208.s n))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record