Problem GT-003 — the Erdős–Gyárfás conjecture

Conjectura.Problems.GT003.Statement

/-
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
-/
import Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.CycleLength
import Mathlib.Combinatorics.SimpleGraph.Finite

/-! # Problem GT-003 — the Erdős–Gyárfás conjecture

LOCKED: solvers cannot modify this file.
-/
namespace Conjectura.GT003
open Conjectura.GraphTheory
/-- 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)
end Conjectura.GT003