Formal target: Corpus.OEIS111291.conjecture

Simon Colton conjectures that the number of refactorable numbers less than $x$ is at least $\frac{x}{2\log x}$.

Exact formal statement

Filter.Eventually.{0}
  (fun x =>
    GE.ge.{0} (Nat.cast.{0} (Corpus.OEIS111291.countRefactorable x))
      (HDiv.hDiv.{0, 0, 0} x (HMul.hMul.{0, 0, 0} 2 (Real.log x))))
  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