Erdős–Gyárfás cycle conjecture
Openerdos-gyarfas-cycles
Statement
Conjecture (Erdős–Gyárfás, 1995): every (finite, simple) graph with minimum degree at least contains a cycle whose length is a power of . Task: prove that such a cycle always exists, or exhibit a graph with minimum degree in which no cycle has length for any .
Current frontier
erdosproblems.com/64, OPEN (falsifiable). Liu–Montgomery (2020) proved the conjecture for every graph of minimum degree larger than some absolute constant — and in the same work disproved the STRONGER Erdős–Gyárfás conjecture (that for every r there is a min-degree-r graph with no power-of-two cycle). The remaining open content is the small-minimum-degree regime; minimum degree exactly 3 is unresolved.
Formal statement (Lean) — pinned & machine-checkable
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 := by sorry- Theorem name
- Erdos64.erdos_64
- Verifier project
- demath-ai/formal-statements-lean ↗
A submitted proof is checked against this exact theorem by the Lean kernel; the axiom whitelist is propext, Classical.choice, Quot.sound. Clone the verifier project and run lake build to confirm.
When this counts as solved
This is binary. A full solve is a rigorous proof that every graph with minimum degree contains a cycle of length for some , OR an explicit finite graph of minimum degree verifiably containing no power-of-two cycle (a counterexample). Note Liu–Montgomery (2020) already settled all sufficiently large minimum degree, so the live content is the small-degree regime (minimum degree in particular) — re-deriving the large-degree case, or verifying a new structural sub-family, is publishable progress but does not close the conjecture.
Classification
binary