Formal target: Corpus.OEIS40.conjecture

**Conjecture from Thomas Ordowski (2023)**: $\log \log a(n+1) - \log \log a(n) < 1/n$ for $n > 0$.

Exact formal statement

∀ (n : Nat),
  LT.lt.{0} 0 n →
    LT.lt.{0}
      (HSub.hSub.{0, 0, 0} (Real.log (Real.log (Nat.cast.{0} (Corpus.OEIS40.a (HAdd.hAdd.{0, 0, 0} n 1)))))
        (Real.log (Real.log (Nat.cast.{0} (Corpus.OEIS40.a n)))))
      (HDiv.hDiv.{0, 0, 0} 1 (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