# Barnette’s Hamiltonian-cycle conjecture

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Paired states and Hamiltonian cycles in cubic bipartite planar graphs](../../preprints/Paired-states-and-Hamiltonian-cycles-in-cubic-bipartite-planar-graphs-September-24-2026/paper.pdf)

## Scope

Barnette's conjecture states that every finite simple cubic bipartite planar graph that is 3-vertex-connected has a Hamiltonian cycle. The formalization proves this statement for every such graph. The selected result is the existence of a cycle visiting every vertex exactly once.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Barnette's Hamiltonian-cycle conjecture | [BarnetteHamiltonian.lean](../ComparatorChallenges/BarnetteHamiltonian.lean) |