Problem GT-003 — the Erdős–Gyárfás conjecture
goaldef
Every graph with minimum degree at least three contains a cycle whose length is a power of two. Known for graphs with no K₄ minor, and for large girth; open in general.
def goal : Prop :=
∀ (V : Type) [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj],
(∀ v : V, 3 ≤ G.degree v) → ∃ k : ℕ, HasCycleLength G (2 ^ k)Builds on
From Mathlib
import Conjectura.Problems.GT003.Statement · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors