Formal target: Corpus.OEIS84046.conjecture

Conjecture: if a(k) = 0 then k is an even square.

Exact formal statement

∀ (k : Nat),
  Eq.{1} (Corpus.OEIS84046.a k) 0 → Exists.{1} fun m => Eq.{1} k (HPow.hPow.{0, 0, 0} (HMul.hMul.{0, 0, 0} 2 m) 2)

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

Environment availability: available.