Formal target: Corpus.Erdos126.erdos_126.variants.isLittleO

Erdős says that $f(n) = o(\frac{n}{\log n})$ has never been proved.

Exact formal statement

∀ (f : Nat → Nat),
  Corpus.Erdos126.IsMaximalAddFactorsCard f →
    Asymptotics.IsLittleO.{0, 0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (f n)) fun n =>
      HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} n) (Real.log (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