Formal target: Corpus.OEIS115366.conjecture

Conjecture: $a(n)/A006880(n) \rightarrow 1.77...$ where A006880(n) is the number of primes $\le 10^n$.

Exact formal statement

Exists.{1} fun L =>
  And
    (Filter.Tendsto.{0, 0}
      (fun n =>
        HDiv.hDiv.{0, 0, 0} (Nat.cast.{0} (Corpus.OEIS115366.a n))
          (Nat.cast.{0} (HPow.hPow.{0, 0, 0} 10 n).primeCounting'))
      Filter.atTop.{0} (nhds.{0} L))
    (And (LE.le.{0} 1.77 L) (LE.le.{0} L 1.78))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record