A few days ago, OpenAI released a preprint presenting a proof of the cycle double cover conjecture and attributing the proof to GPT-5.6 Sol Ultra (OpenAI 2026). The conjecture asserts that every finite bridgeless undirected graph has a cycle double cover. Its first published formulations date from the 1970s, and it had remained open for more than half a century as one of the major longstanding problems in graph theory.
In two earlier posts—here and here—we considered cycle decompositions that cover every edge exactly once. A cycle double cover allows the cycles to overlap while retaining an exact covering condition. A cycle double cover of a graph is a multiset of cycles such that every edge of belongs to exactly two members of , counted with multiplicity. Thus, the same cycle may occur more than once. A bridge is an edge whose deletion increases the number of connected components. Since a bridge lies on no cycle, every graph admitting a cycle double cover must be bridgeless.
The assertion that this necessary condition is also sufficient became known as the cycle double cover conjecture. It was formulated independently in published work by Szekeres (Szekeres 1973), Itai and Rodeh (Itai and Rodeh 1978), and Seymour (Seymour 1979). It is also commonly attributed to Tutte; see Jaeger’s survey (Jaeger 1985).
Several broad classes of graphs were already known to satisfy the conjecture. A graph is planar if it can be drawn in the plane so that edges meet only at common endpoints. Once such a drawing is fixed, the connected regions of the complement are called its faces. In a plane drawing of a bridgeless graph, every facial boundary walk can be decomposed into cycles, and every edge occurs twice among the facial boundaries. These cycles therefore form a cycle double cover (Jaeger 1985).
A graph is cubic if every vertex has degree three. A proper -edge-colouring assigns one of three colours to every edge so that adjacent edges receive different colours. In a properly -edge-coloured cubic graph, the union of any two colour classes is -regular and hence a disjoint union of cycles. The three pairwise unions form a cycle double cover, since every edge belongs to exactly two of them (Szekeres 1973).
A connected graph is -edge-connected if deleting fewer than edges leaves it connected. Jaeger’s -flow theorem implies that every -edge-connected graph has a cycle double cover (Jaeger 1979).
Other substantial special cases were also known. A Hamiltonian path is a path containing every vertex of the graph. Tarsi proved that every bridgeless graph with a Hamiltonian path has a cycle double cover (Tarsi 1986). A graph is locally connected if, for every vertex , the subgraph induced by the neighbours of is connected. Kriesell proved the conjecture for all bridgeless locally connected graphs (Kriesell 2006).
A -factor is a spanning -regular subgraph and is therefore a disjoint union of cycles. The oddness of a bridgeless cubic graph is the minimum number of odd cycles occurring in any of its -factors. Huck proved that every bridgeless cubic graph of oddness at most four has a cycle double cover (Huck 2001).
The main result stated in the OpenAI preprint is the following.
The proof of Theorem begins with the standard reduction to loopless cubic multigraphs. Parallel edges are permitted, and a pair of parallel edges is regarded as a cycle. Put the three-dimensional vector space over the field with two elements. After choosing an orientation of every edge, a -flow is a map such that, at every vertex, the sum of the values on the outgoing edges equals the sum of the values on the incoming edges. The flow is nowhere-zero if for every edge . A classical result guarantees the existence of such a flow on every bridgeless graph.
At each cubic vertex, the three incident flow values , , and are nonzero and satisfy The key new step is to assign to every edge a two-element set such that, for every vertex and every , In other words, each element of occurs in either none or exactly two of the sets attached to the edges incident with a given vertex.
Such assignments can be constructed locally at each vertex, but the two endpoints of an edge need not initially prescribe the same set. The proof encodes these compatibility conditions as a linear system over . A duality argument then shows that this system always has a solution, making the local assignments consistent across the entire graph.
For each , define The defining condition on the sets ensures that every vertex has degree either zero or two in the subgraph with edge set . Consequently, each is a disjoint union of cycles. Moreover, every edge belongs to exactly two of the sets , because contains exactly two elements. Taking all the cycle components of the subgraphs , with multiplicity, therefore produces a cycle double cover of .