Erdős problem 64

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

64.lean

Retained formal statement1 of 1

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

FormalConjectures/ErdosProblems/64.leanErdos64.erdos_643 linesExact file

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

OpenStatement only, no proof