Formal target: Corpus.OEIS4290.conjecture

It is known that $a(10^k - 1) = (10^{9k} - 1) / 9$ for all $k$.

Exact formal statement

∀ (k n : Nat),
  LT.lt.{0} n (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 10 k) 1) →
    LT.lt.{0} (Corpus.OEIS4290.a n) (Corpus.OEIS4290.a (HSub.hSub.{0, 0, 0} (HPow.hPow.{0, 0, 0} 10 k) 1))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record