Formal target: Corpus.OEIS120424.conjecture1

Conjecture (1): The natural density of even terms in the sequence is $1/2$.

Exact formal statement

Filter.Tendsto.{0, 0}
  (fun n =>
    HDiv.hDiv.{0, 0, 0}
      (Nat.cast.{0}
        (Finset.card.{0}
          (Finset.filter.{0} (fun k => Eq.{1} (HMod.hMod.{0, 0, 0} (Corpus.OEIS120424.a k) 2) 0) (Finset.range n))))
      (Nat.cast.{0} n))
  Filter.atTop.{0} (nhds.{0} (1 / 2))

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

Environment availability: available.

Public accepted solutions (paginated API)

Public JSON record