The Lovász–Plummer conjecture (proved 2011) and Sheehan's conjecture

Conjecture · sheehan_conjecture

**Sheehan's conjecture (1977).**

Every $4$ -regular graph with a Hamiltonian cycle has a second Hamiltonian cycle (one with a different edge set). Sheehan's conjecture would settle the last open case of the question, raised by Smith's theorem for cubic graphs, of which regular Hamiltonian graphs have a second Hamiltonian cycle: Thomassen [Th98] proved it for all $r$ -regular graphs with $r \ge 300$ .

Formal statement · Lean 4.lean

theorem sheehan_conjecture :
    ∀ {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj],
      (∀ v, G.degree v = 4) →
      ∀ (v : V) (c : G.Walk v v), IsHamiltonianCycle G c →
        ∃ (w : V) (c' : G.Walk w w), IsHamiltonianCycle G c' ∧
          c'.edges.toFinset ≠ c.edges.toFinset := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗