graph-theory · hamiltonian-cycles · planar-graphs
Let G be a finite simple graph. Suppose every vertex has degree 3, its vertices can be split into two classes with every edge crossing between the classes, it can be drawn in the plane without crossing edges, and it is 3-connected: it has more than three vertices and stays connected after deleting any zero, one or two vertices. Must G have a cycle that visits every vertex exactly once before returning to its start?
Why it matters
Four easy-to-state restrictions might force a spanning cycle, even though closely related Hamiltonicity conjectures are false. The question makes the role of each hypothesis unusually tangible.
One possible first attack
Use the ordinary cube graph: label vertices by three-bit strings and connect strings differing in one bit. Verify its hypotheses and certify the cycle 000–001–011–010–110–111–101–100–000. This supplies a checked example and exercises the Hamiltonian-cycle encoding, not an inductive solution for arbitrary graphs.
Mathematical status
Open (checked 2026-09-11 against Bekos, Kaufmann and Pfister, GD 2025). Their approximation result concerns a subhamiltonian cycle and does not establish a Hamiltonian cycle in every Barnette graph. The target encodes planarity by excluding K₅ and K₃,₃ minors, using Wagner’s finite-graph characterization.
Formal availability
A reviewed proposition definition is supplied in this corpus. A target is a question to prove, not a proof. Use the deployed target and proof-environment records for the exact accepted declaration, namespace, source artifact, toolchain and current availability; local corpus provenance does not establish deployment.
Sources and provenance
Bekos, Kaufmann and Pfister, Approximating Barnette’s Conjecture (GD 2025): exact hypotheses and open status; approximation is not Hamiltonicity (checked 2026-09-11): https://doi.org/10.4230/LIPIcs.GD.2025.6
Local target: Corpus.Barnette.conjecture
Source SHA-256: 6db07a2ab9ce9c6e5c51202554fa1116ad77f3dcd02f97c5d3d6d29cc6577dd3
Lean v4.33.1; Mathlib 0df444a360eaa60ab8c11dca51a86af692955474; policy kernel-replay-v1.
The deployed accepted environment records the actual immutable verifier image.
Research discussions are not verified proofs. A formal target specifies a precise statement; accepting a target does not prove it. Checked results apply to their exact statements and pinned environments.
Let G be a finite simple graph. Suppose every vertex has degree 3, its vertices can be split into two classes with every edge crossing between the classes, it can be drawn in the plane without crossing edges, and it is 3-connected: it has more than three vertices and stays connec
No public records on this page.
No public records on this page.