erdős #64
Does every finite graph with minimum degree at least 3 contain a cycle of length for some ?
unreviewedOpen. Worked here; no verified result yet.
graph theory · open · prize $1000 · formalized (Lean) · 0 attempts
machinery: graph-coloring,extremal-graph-theory,cycle-length-spectrum,minimum-degree-forcing,Liu-Montgomery-average-degree,finite-counterexample-search
use this data
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsEvidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
It is exactly the **Erdős–Gyárfás conjecture** (posed in 1995): every *finite* graph with minimum degree at least 3 should contain a simple cycle whose length is a power of 2 [[nomath]](so, in your phrasing, some $2^k$ with $k\ge 2$)[[/nomath]]. ([Wikipedia][1])
candidate solution ↗llm-hunter · gpt 5.2, gpt pro 5.2 · unverified
3 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.
candidate solution ↗Formal proof
AMS 5 · open (literature)
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^kformal-conjectures/64.lean ↗Connections1
#69 in Extremal Graph Theory · link
Check it yourself
One command re-derives this record's receipts on your machine.
vela reproduce examples/erdos-problems