Barnette's conjecture
Barnette's conjecture asserts that every cubic bipartite polyhedral graph has a Hamiltonian cycle. A polyhedral graph is one that is planar and 3-vertex-connected. A manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claims a proof. This page summarizes the published claim and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- According to the manuscript's introduction, the conjecture was recorded by Grünbaum in the 1969 Waterloo proceedings. It places the problem in the line of questions begun by Tait's conjecture for cubic polyhedral graphs, which Tutte disproved in 1946.
- The same introduction lists earlier partial results. Goodey proved the case where all faces are quadrilaterals or hexagons. Feder and Subi allowed large faces in one of the three face classes. Kardoš proved the related Barnette–Goodey conjecture for faces of size at most six. T. Schnieders proved the case of faces of size at most eight (arXiv:2508.03531).
The original result
- Claim. Every finite simple cubic bipartite planar 3-vertex-connected graph has a Hamiltonian cycle. The proof works in the dual triangulation. It partitions the triangulation's vertices into two sets, each inducing a tree, with a prescribed facial edge's endpoints in one class. The manuscript derives two consequences. The Hamiltonian cycle can be chosen to avoid any given edge. And every three-edge path in a finite simple cubic 3-vertex-connected Pfaffian bipartite graph lies in a Hamiltonian cycle, through an equivalence of Gorsky, Steiner and Wiederrecht (arXiv:2202.11641).
- Source. Paired states and Hamiltonian cycles in cubic bipartite planar graphs in the openai/math repository (commit
1581d4c). - Formalization, as described by the repository. The scope note lean/docs/180.md states that the formalization proves the statement for every finite simple cubic bipartite planar 3-vertex-connected graph. The selected result is the existence of a cycle that visits every vertex exactly once. The comparator statement is BarnetteHamiltonian.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 15 October 2026) |
|---|---|---|---|---|
| 2026-10-09 | Cameron Nottingham, cjnott1999/barnette-conjecture | Reading and use | The record of an AI-assisted research programme on the conjecture. It states that the programme had not proved the conjecture and verified OpenAI's proof independently on the day it appeared. It includes a report with a walk-through of that proof and a worked example, equivalent forms of its existence statement, and a new proof that every leapfrog of a Barnette graph is Hamiltonian. The README notes that this last theorem already follows from Feder and Subi (2006). Since 6 October the programme has worked towards finding a Hamiltonian cycle in polynomial time. | A snapshot of the working repository taken on 9 October 2026. The README states that AI agents did most of the derivations, computations and audits. |
| 2026-10-11 | formal-conjectures pull request #7149 | Formal statement | Adds Barnette's Hamiltonian-cycle statement, with its four hypotheses explicit, to Google DeepMind's Formal Conjectures repository, and records it as solved by the manuscript. | Open pull request. Its description states that the external proof was not built or run through the comparator, so no formal-proof attribute is added, and that it was prepared with AI assistance. |
| 2026-10-14 | Erebos Labs, erebos-labs/family180-paired-state-audit (release v1.1.0) | Support (finite checks) | An exact executable audit of the manuscript's paired-state cancellation on small examples: bipyramids, a coned cube and, in v1.1.0, a 12-vertex octahedron edge expansion that exercises a complete reversal orbit. | The README states that the general theorem is already formalized upstream and that the audit claims no new theorem or new Lean verification. It also notes that some checks in the v1.0.0 examples are vacuous. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.