Source and verification
This article explains family 180 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.
🏷️ Hamiltonian cycles and planar hypotheses
A Hamiltonian cycle visits every vertex exactly once. A cubic graph has degree three at every vertex; a bipartite graph has a partition into two independent vertex classes. A graph is three-vertex-connected if it has at least four vertices and remains connected after deleting any two vertices.
Manuscript claim
Every finite simple cubic bipartite planar three-vertex-connected graph has a Hamiltonian cycle. (OpenAI, 2026)
This is Barnette’s conjecture. All four structural hypotheses belong to the statement. A spanning subgraph of degree two is insufficient: it can be a union of several cycles. The central issue is obtaining one connected spanning cycle.
For an elementary example, the cube graph is cubic, bipartite, planar, and three-vertex-connected. A cyclic Gray code on its eight binary words supplies a Hamiltonian cycle, changing one coordinate at each step. The manuscript treats the entire class, with no bound on face size.
🏷️ The dual induced-tree problem
Embed the graph on the sphere and form its planar dual. Cubic vertices become triangular faces. The original bipartition colors those triangles black and white, with opposite colors across each edge.
The relevant dual characterization asks for a partition of the dual vertices into two sets, each inducing a tree. “Inducing” means retaining every edge whose endpoints belong to the set; choosing a convenient spanning tree inside a denser induced subgraph does not suffice.
The manuscript proves a strengthened partition statement with a prescribed pattern on any chosen facial triangle: two specified adjacent vertices belong to one part and the third to the other. This local prescription allows partitions of smaller triangulations to be glued across separating triangles. It also yields a Hamiltonian cycle avoiding any one prescribed edge in the original graph.
The local condition is therefore part of the induction invariant. Proving only an unspecified partition of each smaller piece could leave incompatible choices along their common boundary.
🏷️ Paired incidence states
Choose a black triangle as the outer face and call its vertices roots. The remaining black triangles and nonroot vertices have equal cardinality. A state assigns to each remaining black triangle one incident vertex, using each nonroot vertex exactly once. It is a perfect matching in a face-vertex incidence graph.
A pair of states makes different choices at every triangle. For the second state , let consist of the edge opposite its chosen vertex in each black triangle. The immediate objective is to find a pair for which is a forest.
In the case without separating triangles, a planar density bound and an integral flow first produce paired states. A disk-counting identity then controls signs associated with cycles. These are the inputs to a finite weighted sum over all pairs.
🏷️ Two ways to group one finite sum
The proof analyzes the same exponential sum in two different orders.
First fix the second state . If contains a cycle, reversing the appropriate cycle changes the first state while preserving the second. The disk identity gives opposite phases to the paired terms. Their real weights agree because those weights depend only on . Thus every contribution associated with cyclic cancels.
This cancellation does not yet prove that any forest state exists: the entire sum might be zero. The second grouping supplies nonvanishing.
Join the two chosen vertices inside each black triangle and fix the resulting undirected edge set . Its components are cycles, and the compatible pairs correspond to independent choices of their orientations. Positive circulations on spokes from face centers provide real weights favoring one orientation of each cycle.
Each cycle contributes a simple zero as the exponential parameter tends to zero. Among groups with the fewest cycles, the disk identity aligns the leading phases, while their leading magnitudes are positive. Those lowest-order contributions cannot cancel. The full sum is consequently nonzero, so at least one uncanceled forest state remains.
The method uses cancellation to exclude unwanted states and positivity of leading terms to retain a wanted one. Either argument alone would be incomplete.
🏷️ From a forest to one spanning cycle
A forest state has three components, each containing one root. Planar tree duality turns the complementary structure into a tree on the white faces. The resulting selected edges include one edge at every black and white face, and the disk identity proves they are acyclic.
Their complementary dual is connected and has degree two at every vertex. A finite connected graph of degree two is a single cycle, giving precisely the global property that a generic two-factor lacks. The two regions on its sides identify the required induced trees.
When a separating triangle exists, split along it and apply induction to the two smaller triangulations with matching prescribed facial patterns. The induced trees glue along a vertex or an edge, preserving both connectedness and acyclicity.
The sum is finite but can be enormous. The manuscript uses it for existence and does not assert a polynomial-time algorithm for finding the Hamiltonian cycle.
🏷️ Key steps and proof outlines
The state condition fixes the disk’s signed boundary
Consider a simple directed cycle made by choosing, in each used black triangle , an edge from its state-assigned vertex to another vertex. Let be its length, the number of interior vertices, the black and white interior face counts, and the number of boundary edges whose black face is inside. The roots lie on the outer boundary and have no outgoing chosen edges, so none is inside this cycle. (OpenAI, 2026)
Euler’s formula and signed side counting give
The state bijection supplies the extra equation : every interior vertex is matched to an interior black face, and exactly the designated boundary vertices are matched to black faces inside. Substitution yields . Thus a counterclockwise cycle has signed edge sum , and a clockwise one has . This conclusion does not hold for an arbitrary cycle without the matching condition.
A fixed second state gives a sign-reversing involution
For a pair of states, direct the edge in every black triangle. Each nonroot vertex has indegree and outdegree one, so these edges form disjoint simple cycles. Let
where is the signed boundary function and will be chosen later. The disk identity makes an integer.
Fix for which the opposite-edge graph has a cycle, and choose one such cycle using only . For a partner , orient those opposite edges from toward the third vertex . Each vertex has at most one outgoing edge, so the chosen undirected cycle must be directed. Replacing by around the cycle cyclically permutes assigned vertices, preserving the state bijection and reversing the cycle. It is an involution without fixed points.
The local change obeys . Summing around the cycle and applying the disk identity gives a change of equal to . Therefore the complex phase changes sign, while is unchanged. All terms with this cyclic second state cancel exactly.
Positive circulation prevents the entire sum from vanishing
Place a center in each black triangle and draw its three incidence spokes. Assign antisymmetric spoke weights so that every bounded face has circulation one. Such weights exist: route one unit from each bounded dual face to the unbounded face; intermediate contributions cancel. The circulation around any simple counterclockwise spoke cycle is then the positive number of enclosed faces.
Now regroup pairs by their undirected chosen-edge set . The pairs in one group are exactly the independent orientation choices on the cycles of . For a cycle , let and be the sums of the weights at its heads in the two orientations. Replacing each edge by the two-spoke detour gives
The detoured curve remains simple: only one edge per black triangle is used, so detours have disjoint interiors, and each can be slid across a triangle subdisk excluding its third corner. The cycle’s orientation is preserved.
The group’s contribution is consequently
Each factor has a simple zero at . If has cycles, its first nonzero coefficient is
Choose the smallest cycle count occurring among groups. Every contribution at that degree has the same phase and strictly positive magnitude; groups with more cycles contribute nothing at that degree. Thus is not identically zero. Since every cyclic group canceled in the first grouping, some surviving state has a forest.
Preserve the prescribed boundary when passing to the Hamiltonian cycle
The forest has one component through each of the three roots. The source’s planar dual construction uses its complement to build a tree on the white faces, selecting one edge at each face. A second disk-identity argument excludes cycles among the selected edges. The complementary dual is connected and has degree two at every vertex, hence is one spanning cycle. Connectedness is the step that upgrades a two-factor to a Hamiltonian cycle.
The prescribed pattern on the outer triangle determines how its roots are allocated. When a separating triangle occurs, apply induction to the two pieces with compatible prescribed patterns. The corresponding induced trees meet along a vertex or an edge, so gluing preserves acyclicity and connectedness. This explains why the strengthened facial statement is carried through the proof, rather than added after an unprescribed existence theorem.
See Also
- Cycle-and-edge decompositions permits many edge-disjoint cycles; Barnette’s problem requires one cycle through every vertex.
- Double-dimer loops gives another setting where the union of two matchings decomposes into independently orientable cycles.
🏷️ Manuscripts and verification scope
- Paired states and Hamiltonian cycles in cubic bipartite planar graphs — pinned manuscript and companion source.
The family scope page describes selected formalization coverage. The selected statement is existence of a Hamiltonian cycle under all four graph hypotheses. It does not separately document the edge-avoidance or Pfaffian consequences. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.
OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.