A tour of every corner?
A preprint claims Barnette’s conjecture: every cubic polyhedron whose corners can be colored black and white along every edge has a Hamiltonian cycle
Covers result 180 in OpenAI’s catalog: its one paper. See its connections to other results and the work it cites.
5:48. English captions available. The video loads from YouTube when you press play.
Chapters
The claim, in plain words
Take a polyhedron where three edges meet at every corner, like a cube. A Hamiltonian cycle is a closed tour along its edges that visits every corner exactly once; the cube has 6. Tait conjectured that every such polyhedron has one. Tutte disproved it in 1946 with a polyhedron of 46 corners; our exhaustive search confirms that it has no tour. Each of its three large pieces forces the tour through its own edge to the centre corner, but a tour uses only two of the three. Tutte’s polyhedron has faces with an odd number of sides. Barnette’s conjecture forbids that: if the corners can be colored black and white so that every edge joins opposite colors, which means every face has an even number of sides, as on the cube or a hexagonal prism, then a tour always exists.
As the paper recounts, the conjecture was recorded by Grünbaum in the proceedings of a 1968 Waterloo conference, published in 1969. Goodey proved it when every face is a square or a hexagon, Feder and Subi allowed faces of any size in one of three face colors, if the other two have only squares and hexagons, and in 2025 Schnieders proved it when no face has more than 8 sides. In our own check, every such polyhedron with up to 20 corners (15 of them) has a tour. Turned inside out, a reformulation going back to Stein and to Alt, Payne, Schmidt and Wood, each face becomes a dot and each corner a black or white triangle, and a tour corresponds to splitting the dots into two groups that each form a tree, counting every edge among their dots; the tour runs along the boundary between them.
Result 180 is one OpenAI preprint, Paired states and Hamiltonian cycles in cubic bipartite planar graphs (11 pages, dated September 24, 2026). Its Theorem 1.1: “Every finite simple undirected graph that is cubic, bipartite, planar, and 3-vertex-connected has a Hamiltonian cycle.” Its Corollary 7.1: for every edge, some Hamiltonian cycle avoids it, a strengthening already known to be equivalent. Its Corollary 7.2, combined with an equivalence proved by Gorsky, Steiner and Wiederrecht: in every cubic, 3-connected, bipartite graph with a Pfaffian orientation, a class that includes all the planar ones, every path of three edges lies on a Hamiltonian cycle.
What it doesn’t claim
Nothing without the coloring or 3-connectivity: Tutte’s graph shows that the coloring is needed, and our example of three cube-like blocks strung between two corners (26 corners, only 2-connected) has no tour. No algorithm: the proof shows that a certain finite sum of exponentials is not zero, and the paper does not claim a polynomial-time construction. Nothing stronger: on the cube, by our count, 24 of the 72 paths with four edges lie on no tour. The paper reports no computation.
Where it stands
- Posted as a preprint
- OpenAI, 11 pages, dated September 24, 2026
- Peer reviewed
- Not yet
- Checked in Lean
- The theorem, with a topological definition of planarity, formalized by OpenAI; not run by us
Last checked October 19, 2026. The preprint has not been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization whose comparator statement is Theorem 1.1, with planarity defined topologically: points in the plane joined by injective arcs whose interiors do not meet. By our count the proof takes 31 files and 8,936 lines, excluding Mathlib (source); it turns the drawing into a minor of a square grid and argues through algebraic duality. The corollaries are not stated in Lean, and the Pfaffian corollary is not formalized. We found no unproved steps by search; we have not rebuilt the proof. The paper is not among those OSVerify reviewed, and we have seen no expert review.
How the proof goes
- Inside out. Work on the dual triangulation, with black and white triangles. Put one black triangle on the outside; its three corners are the roots.
- States and pairs. A state lets every other black triangle point at one of its own corners, using each remaining dot exactly once; these states come from Tutte’s theory of trinity. A pair is two states that disagree at every black triangle.
- The disk identity. Give each directed edge a sign, +1 if its black triangle is on the left and −1 otherwise. Along any cycle whose edges start where a state points, the signs add to exactly −3 counterclockwise and +3 clockwise, by Euler’s formula and the state’s matching condition.
- A weighted sum. Sum over all pairs, with phase i to the power of a third of the sign total and a weight that depends only on the second state. Pairs of the wrong shape cancel: rotating the first state around a cycle flips the phase and leaves the weight alone.
- It is not zero. Grouping pairs by their cycles, weights on spokes are chosen so that, around every cycle, counterclockwise outweighs clockwise, so the lowest-order terms all have the same phase. Some pair therefore has the right shape, a forest.
- Two trees and the tour. A tree on the white triangles selects one edge at each triangle, and the selected edges split the dots into two induced trees. Separating triangles are handled by cutting and gluing, using the freedom to prescribe an edge. Back on the polyhedron, the boundary between the trees is the tour.
The numbers in the video
- The cube: 6 Hamiltonian cycles; each of its 48 three-edge paths lies on exactly one; 24 of its 72 four-edge paths lie on none.
- Exhaustive searches: Tutte’s 46-corner polyhedron and our 26-corner 2-connected example have no Hamiltonian cycle.
- Every cubic polyhedron with black-and-white corners up to 20 corners (15 graphs): each has a tour, a tour avoiding each edge, and a tour through each three-edge path.
- A suitable pair found by search, then the paper’s tree step: on the truncated octahedron (24 corners; trees of 6 and 8 dots) and the truncated icosidodecahedron (120 corners; faces of 4, 6 and 10 sides; trees of 22 and 40 dots), the output is a Hamiltonian cycle.
- The Lean count: our count of the import closure.
Read the source
- Paired states and Hamiltonian cycles in cubic bipartite planar graphs (PDF), 11 pages.
- The Lean scope note.
- The collection’s catalog, where this is result 180.
The paper
OpenAI groups related papers into one result; this one has a single paper.
Transcript
Read the full script
0:00The question
Take a polyhedron where three edges meet at every corner, like a cube. Can you walk along its edges, visiting every corner exactly once, and return to where you started? Such a closed tour is called a Hamiltonian cycle; the cube has 6. Tait’s conjecture said that every polyhedron with three edges at each corner has one. Tutte disproved it in 1946, with a polyhedron of 46 corners. Our exhaustive search confirms it has no tour: each of its three large pieces forces the tour through its own edge to the centre corner, but a tour uses only two of the three. Tutte’s polyhedron has faces with an odd number of sides. Barnette’s conjecture forbids that: if the corners can be colored black and white so that every edge joins opposite colors, which means every face has an even number of sides, as on the cube or a hexagonal prism, then a tour always exists. The conjecture was recorded by Grünbaum in the proceedings of a Waterloo conference, published in 1969. As the paper recounts, Goodey proved it when every face is a square or a hexagon, Feder and Subi allowed faces of any size in one of three face colors, if the other two have only squares and hexagons, and in 2025, Schnieders proved it when no face has more than 8 sides. In our own check, every such polyhedron with up to 20 corners has a tour. The way in, a reformulation going back to Stein, is to turn the polyhedron inside out. Each face becomes a dot, and each corner becomes a triangle, colored black or white, with opposite colors across every edge. A tour on the polyhedron then corresponds to splitting the dots into two groups that each form a tree, counting every edge among their dots; the tour runs along the boundary between them.
1:51The claim
Result 180 is a single OpenAI preprint, 11 pages long, dated September 24, 2026. Its theorem: every finite simple graph that is cubic, bipartite, planar and 3-connected has a Hamiltonian cycle. That is Barnette’s conjecture. Its proof also gives, for every edge, a tour that avoids it, a strengthening already known to be equivalent. Combined with an equivalence proved by Gorsky, Steiner and Wiederrecht, the paper concludes more: in every cubic, 3-connected, bipartite graph with a Pfaffian orientation, a class that includes all the planar ones, every path of three edges lies on a tour. Not claimed: anything without the coloring or 3-connectivity. Tutte’s graph shows that the coloring is needed, and our example of three cube-like blocks strung between two corners, which is only 2-connected, has no tour. No algorithm: the proof shows that a certain finite sum of exponentials is not zero, and the paper does not claim a polynomial-time construction. And nothing stronger: in our check of the cube, a third of the paths with four edges lie on no tour at all.
3:04How the proof goes
The proof works on the inside-out triangulation. Put one black triangle on the outside; its three corners are the roots. A state lets every other black triangle point at one of its own corners, using each remaining dot exactly once; these states come from Tutte’s theory of trinity. A pair is two states that disagree at every black triangle. The engine is a disk identity. Give each directed edge a sign, plus one if its black triangle is on the left and minus one otherwise. Along any cycle whose edges start where a state points, the signs add up to exactly minus three going counterclockwise and plus three going clockwise. Euler’s formula and the state’s matching condition force it. Now sum over all pairs, giving each pair the phase i to the power of a third of its sign total, times a weight that depends only on the second state. Pairs of the wrong shape cancel. If a certain set of edges contains a cycle, rotating the first state around it changes the phase by a factor of minus one and leaves the weight alone. But the total is not zero. Group the pairs by their cycles, and choose weights on spokes from each black triangle’s centre so that, around every cycle, counterclockwise outweighs clockwise; then the lowest-order terms all point the same way and cannot cancel. So some pair has the right shape, a forest. From it, a tree on the white triangles selects one edge at each triangle, and the selected edges split the dots into the two required trees. Separating triangles are handled by cutting the sphere along them and gluing the halves, using the freedom to prescribe an edge. Back on the polyhedron, the boundary between the trees is the tour. In our computation, a search found a suitable pair on a polyhedron with a hundred and 20 corners, and the paper’s tree step then produced a valid tour.
4:55Where it stands
The preprint is not peer reviewed and has not been revised. OpenAI’s Lean files state the theorem with a genuine topological definition of planarity, a drawing in the plane with non-crossing arcs, and prove it in 31 files and about 9,000 lines, with no gaps we could find by search; we did not run the check. The formal proof turns the drawing into a minor of a square grid and argues algebraically. The Pfaffian corollary is not formalized. The paper is not among those OSVerify reviewed, and we have seen no expert review. If it holds, Barnette’s conjecture is true: on every polyhedron with three edges at each corner, whose corners can be colored black and white with every edge joining opposite colors, you can visit every corner once and come home.
Spot a mistake?
This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.