Proof of Barnette's conjecture on Hamiltonian cycles in cubic bipartite planar graphs
An OpenAI manuscript claims that every cubic, bipartite, planar, 3-connected graph has a Hamiltonian cycle, proving a conjecture recorded in 1969, with a Lean formalization of the full statement attached.
- Lab
- OpenAI
- Model
- Unreleased internal OpenAI model, not named in the release
- Field
- Mathematics
- Date
- 2026-10-06
- Problem posed
- 1969 · open 57 yrs
What was found
Barnette's conjecture, recorded by Grünbaum in the 1969 Waterloo proceedings, is the bipartite survivor of Tait's conjecture, which Tutte disproved in 1946. Earlier work settled it under face-size restrictions: Goodey for faces of size four and six, Feder and Subi for a broader face colouring, and Schnieders in 2025 for faces of size at most eight. The manuscript passes to the dual triangulation, where by the Alt, Payne, Schmidt and Wood formulation Hamiltonicity becomes a partition of the vertices into two induced trees, and analyses one finite exponential sum over pairs of Tutte states in two ways: pairs whose associated edge set contains a cycle cancel in sign, which forces a pair giving a forest. The proof also yields the known equivalent strengthenings that a Hamiltonian cycle can avoid any prescribed edge and that every three-edge path in a cubic 3-connected bipartite Pfaffian graph lies on one. The family's Lean scope document says the formalization proves the conjecture for every such graph.
Novelty check
Read the introduction and Lean scope at commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb on 2026-10-12. Its account of partial results through Schnieders (2025) matches the literature it cites, and no earlier claimed proof was found in the registry. A Hacker News commenter who said they had worked on the conjecture for 24 years reacted to the release in a comment that was quoted widely, but that is reaction rather than a check.
Caveats and known objections
Lean formalization is attached through a Comparator statement, BarnetteHamiltonian.lean, but the catalogue records its review status as unchecked and no outside audit of how the statement encodes planarity and 3-connectivity was found; that encoding is where a formal statement of this conjecture could quietly diverge from the real one. Nobody outside OpenAI is on record as having read the proof. Autonomy is graded ai-led for the same reasons as the other families split from this release.
The open problem
316016
Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
Also recorded at
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
History of this entry
- CorrectedRecorded the vibemathed and MathDB records for this result as registrations. Both list OpenAI's proof as an unreviewed claim, so no grade moved.
- AddedEntered the registry graded Claimed and AI-led.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Community discussion
Graded claimed for verification and ai-led for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Proof of Barnette's conjecture on Hamiltonian cycles in cubic bipartite planar graphs. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-10-06-barnette-conjectureBibTeX
@misc{whataifound-openai-2026-conjecture,
title = {Proof of Barnette's conjecture on Hamiltonian cycles in cubic bipartite planar graphs},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by OpenAI. Verification: Claimed. Autonomy: AI-led.},
url = {https://whataifound.org/finding/2026-10-06-barnette-conjecture}
}