Formal target: Corpus.Erdos82.erdos_82

$F(n) / \log n \to \infty as n \to \infty$

Exact formal statement

Filter.Tendsto.{0, 0} (fun n => HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Corpus.Erdos82.F n)) (Real.log (Nat.cast.{0} n)))
  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