erdos_64

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

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

Recent Submissions

No submissions yet. Be the first to attempt this problem.