Formal target: Corpus.OEIS153330.conjecture1

Conjecture 1: More than half of the terms are 0.

Exact formal statement

LT.lt.{0} (1 / 2)
  (Filter.liminf.{0, 0}
    (fun n =>
      HDiv.hDiv.{0, 0, 0}
        (Nat.cast.{0}
          (Finset.card.{0}
            (Finset.filter.{0} (fun i => Eq.{1} (Corpus.OEIS153330.a i) (Option.some.{0} 0)) (Finset.Icc.{0} 1 n))))
        (Nat.cast.{0} n))
    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