Barnette’s Hamiltonian-cycle conjecture

The explanation

Take the corners and edges of a cube: 8 points and 12 links. Can you walk along the links, visit every point exactly once, and end where you started? Yes. Label the corners with three-digit codes of 0s and 1s, so that linked corners differ in one digit. Then 000, 001, 011, 010, 110, 111, 101, 100 and back to 000 works. A round trip like this is called a Hamiltonian cycle. The cube has exactly six of them.

The cube belongs to a special family. Every point has exactly three links, so the graph is called cubic. Its points split into two teams, with every link joining opposite teams, so it is bipartite. It can be drawn flat with no crossings, so it is planar. And it stays connected even after removing any two points. In 1969, Branko Grünbaum recorded Barnette's conjecture: every graph with all four properties has a Hamiltonian cycle.

The team condition matters. An older guess, Tait's conjecture, asked the same for cubic graphs that are planar and well connected, without teams. William Tutte disproved it in 1946. Barnette's version adds the two-team condition and asks whether that is enough.

Partial answers came by limiting the faces, the regions of the flat drawing. Paul Goodey proved the case where every face has 4 or 6 sides in 1975. Tomás Feder and Carlos Subi allowed large faces in one of three face classes. In 2020, František Kardoš proved a related conjecture with faces of at most 6 sides, using a computer. In 2025, Tobias Schnieders reached faces of up to 8 sides. This paper removes the face-size limit entirely.

The single difficulty is getting one cycle instead of severalSource 1. On the cube, the top square and the bottom square together pass through every point exactly once. But they form two separate loops, not one trip. Local choices can easily produce such a set of loops, and nothing local joins them up.

The paper sidesteps this with a global count. It first redraws the problem on the dual picture, where each face becomes a point and each corner becomes a triangle. Earlier work showed that a Hamiltonian cycle matches a way to split those points into two groupsSource 2. Each group must form a tree, a connected network with no loops. The paper then forms one finite weighted sum over many candidate choices. Choices that would leave a loop cancel each other in pairsSource 3. Grouped another way, the same sum is not zero. So some choice with no loop must exist, and it yields a single round trip.

This makes the proof one of existence. It shows that a Hamiltonian cycle is there, for graphs of any size and any face lengthsSource 4. It does not claim a fast way to find the cycleSource 5. The paper also derives a stronger form: for any single link you name, some Hamiltonian cycle avoids itSource 6.

How sure is this? A computer proof checker called Lean has checked a formal version of the main theorem, for every such graph. A tool called Comparator matches it against a fixed reference statement. No specialist review of the paper has been published.

What it doesn't show. This does not give a fast method for finding the cycle.