Formal target: Corpus.OEIS180017.conjecture

"This sequence is positive on average, since 1/log(3) > 1/log(4).

Exact formal statement

∀ (z : Int), Set.Infinite.{0} (Set.ofPred.{0} fun n => Eq.{1} (Corpus.OEIS180017.a n) z)

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record