Barnette's conjecture
A graph is cubic if every vertex has degree three, and polyhedral if it is planar and 3-vertex-connected, that is, the graph of a convex polyhedron. Tait conjectured that every cubic polyhedral graph is Hamiltonian; Tutte disproved this in 1946. Barnette's conjecture restricts to bipartite graphs. Known before this work: all faces of size 4 or 6 (Goodey), arbitrary faces in one face color class with only quadrilaterals and hexagons in the other two (Feder-Subi), and all faces of size at most 8 (Schnieders, 2025). Does every finite simple cubic bipartite planar 3-vertex-connected graph have a Hamiltonian cycle?
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Argument
- Field
- Graph theory: Hamiltonian cycles in planar graphs
- Posed by
- David Barnette; recorded by Branko Grunbaum as Unsolved Problem 5 in Recent Progress in Combinatorics (Proceedings of the Third Waterloo Conference, May 1968), Academic Press, 1969
- Year posed
- 1969
- Years open
- 57y
- Solved
- 2026-09-24
- Model
- Unreleased internal OpenAI model
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Collection
- OpenAI math release (October 2026), version adc7f12
- Significance
- 48 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Theorem 1.1: every finite simple cubic bipartite planar 3-vertex-connected graph has a Hamiltonian cycle. In the dual triangulation (Stein; Alt-Payne-Schmidt-Wood) the paper splits the vertices into two induced trees with a prescribed facial pattern, using Tutte states, a signed exponential sum over pairs of states, and gluing along separating triangles. Corollaries: the Hamiltonian cycle can avoid any prescribed edge (a known equivalent strengthening, via Kelmans, Hertel and Gorsky-Steiner-Wiederrecht), and every three-edge path in a cubic 3-connected Pfaffian bipartite graph lies in a Hamiltonian cycle. The result is confined to the bipartite polyhedral class.
What the AI did
The OpenAI math release (github.com/openai/math, commit adc7f12) states that its results were produced by an unreleased internal OpenAI model under one fixed procedure, averaging about three hours of ChatGPT Pro thinking compute per result, across roughly 4,000 posed problems; outputs were then grouped into families and filtered for significance. This result is not among the README's stated exceptions (the Riemann zeta zero-free region work and the Hodge conjecture for CM abelian varieties). The manuscript is credited to OpenAI alone and names no human author.
Verification
No independent mathematician has checked this yet. Checked here: the abstract, introduction and Theorem 1.1 of the TeX source; the proof was not refereed. Lean: the challenge BarnetteHamiltonian (OAI.Barnette.main, solution module OAI/Combinatorics/Hamiltonian/Main.lean) is not in the release's formalization catalogue, but its JSON and solution file exist at the pinned commit. Statement read here: every finite simple graph that is 3-regular, bipartite, planar (a crossing-free embedding in by injective arcs with disjoint interiors) and 3-vertex-connected (at least four vertices, connected after deleting any two) has a Hamiltonian cycle, a single closed walk through every vertex once. That is the headline claim. Permitted axioms: propext, Quot.sound, Classical.choice. Not rebuilt here.