Combinatorics·OpenAI Math·Result 180·Lean formalisation listed
Barnette’s Hamiltonian-cycle conjecture
One of the 372 results in OpenAI's public mathematics catalogue, filed under combinatorics: 1 preprint, the latest dated 24 September 2026. This page quotes OpenAI's own summary of the claim, links the paper and abstract, and embeds the animation.
What OpenAI claims
Proves that every finite simple cubic bipartite planar 3-vertex-connected graph has a Hamiltonian cycle, resolving Barnette's conjecture. Equivalently, every three-edge path in a finite simple cubic 3-vertex-connected bipartite Pfaffian graph lies in a Hamiltonian cycle. (Lean)
Paper
Paired states and Hamiltonian cycles in cubic bipartite planar graphs
We prove Barnette's conjecture: every finite simple cubic bipartite planar 3-vertex-connected graph has a Hamiltonian cycle.
Status
Preprint. The paper has not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it. If a video exists, it illustrates the statement; it is not the proof.
The video
Barnette's Conjecture: Does This Loop Always Exist? · Short · 0:40 · description, sources and transcript →
Related results in Combinatorics
- 181The Erdős–Gallai cycle-decomposition conjectureVideoLean
- 182Power savings for intersective polynomial differences and prime argumentsLean
- 183Power savings for planar halving lines and k-setsLean
- 184Correspondence coloring with a fixed forbidden subgraphLean
- 185Counterexamples to infinite matroid intersection and packing/coveringLean
- 186Uniform influence and sharp thresholds for graph and hypergraph propertiesLean
