Hamiltonian cycles

TheoremDirac's theorem#✓fully proved

Let \(G\) be a finite simple graph with \(n \ge 3\) vertices in which every vertex has degree at least \(n/2\). Then \(G\) is Hamiltonian, that is, it has a cycle that visits every vertex exactly once.

theorem dirac {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (hcard : 3 ≤ Fintype.card V)
    (hdeg : ∀ v : V, Fintype.card V ≤ 2 * G.degree v) :
    G.IsHamiltonian

Sources

• G. A. Dirac, Some Theorems on Abstract Graphs, Proc. London Math. Soc. s3-2 (1952), 69–81, DOI 10.1112/plms/s3-2.1.69.

TheoremA cyclic listing of the vertices gives a Hamiltonian cycle#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), and let \(v_0, v_1, \dots, v_n\) be a list of vertices with \(v_0 = v_n\) in which \(v_{i-1}\) and \(v_i\) are adjacent in \(G\) for each \(1 \le i \le n\). If \(v_1, \dots, v_n\) are pairwise distinct, every vertex of \(V\) is among them, and \(n \ge 3\), then \(G\) is Hamiltonian: it has a cycle that visits every vertex exactly once.

public theorem IsHamiltonian.of_cyclic_list {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) (l : List V) (hne : l ≠ [])
    (hclosed : l.head hne = l.getLast hne) (hchain : l.IsChain G.Adj)
    (hnodup : l.tail.Nodup) (hmem : ∀ v, v ∈ l.tail)
    (hthree : 3 ≤ l.length - 1) : G.IsHamiltonian

Used by 2

Used byOre's theorem · A cyclic listing by square adjacencies gives a Hamiltonian square

TheoremOre's theorem#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\) with \(|V| \ge 3\). If \(\deg u + \deg v \ge |V|\) for every pair of distinct nonadjacent vertices \(u\) and \(v\), then \(G\) is Hamiltonian.

theorem ore {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj]
    (hcard : 3 ≤ Fintype.card V)
    (hdeg : ∀ u v : V, u ≠ v → ¬G.Adj u v →
      Fintype.card V ≤ G.degree u + G.degree v) :
    G.IsHamiltonian

Sources

• O. Ore, Note on Hamilton Circuits, Amer. Math. Monthly 67 (1960), 55, DOI 10.2307/2308928.

Uses 1

Proof usesA cyclic listing of the vertices gives a Hamiltonian cycle

DefinitionPrism-Hamiltonicity conjecture for 3-connected planar graphs#✓fully proved

For every finite simple graph \(G\) that is \(3\)-vertex-connected and straight-line planar, the prism \(G \mathbin{\square} K_2\), the Cartesian product of \(G\) with the complete graph on two vertices, is Hamiltonian.

def conjecture : Prop :=
  ∀ (V : Type) (_ : Fintype V) (_ : DecidableEq V)
      (G : SimpleGraph V) (_ : DecidableRel G.Adj),
    SimpleGraph.IsVertexConnected 3 G → SimpleGraph.IsPlanar G →
      (G □ SimpleGraph.completeGraph (Fin 2)).IsHamiltonian

Uses 2 · Used by 1

Statement usesStraight-line planar graph · \(k\)-vertex-connected graph

Used byŠpacapan's counterexample to prism-Hamiltonicity

TheoremŠpacapan's counterexample to prism-Hamiltonicity#●ready to prove

The prism-Hamiltonicity conjecture for 3-connected planar graphs is false: there is a finite simple graph \(G\) that is \(3\)-vertex-connected and straight-line planar whose prism \(G \mathbin{\square} K_2\) is not Hamiltonian.

public theorem_wanted conjecture_refuted : ¬ conjecture

Sources

• S. Špacapan, A counterexample to prism-hamiltonicity of 3-connected planar graphs, Journal of Combinatorial Theory, Series B 148 (2021), 46–52, https://arxiv.org/abs/1906.06683.

Uses 1

Statement usesPrism-Hamiltonicity conjecture for 3-connected planar graphs

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.