Erdős Problem 64

Reference: erdosproblems.com/64

theorem Erdos64.erdos_64 : (∀ (V : Type u_1) (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj], G.minDegree ≥ 3 → ∃ (k : ℕ) (v : V) (c : G.Walk v v), k ≥ 2 ∧ c.IsCycle ∧ c.length = 2 ^ k) ↔ sorry

Does every finite graph with minimum degree at least $3$ contain a cycle of length $2^k$ for some $k \geq 2$?