Monthly Archives: July 2026

The cycle double cover theorem

Posted on by
Reply

This is a guest post by Johannes Carmesin.

You have probably all heard that OpenAI announced a fully automated proof of the cycle double cover conjecture, which was conjectured independently by Tutte, Itai and Rodeh, Szekeres, and Seymour about fifty years ago.

First, to answer the most immediate question: yes, the proof is correct.

Here, I would like to do two things:

  1. explain the statement of the theorem; and
  2. give an overview of how the proof has been verified.

Statement of the theorem

The theorem has a particularly appealing topological formulation: every bridgeless multigraph can be embedded in a pseudosurface in such a way that every face is a disc. In particular, every edge occurs exactly twice among the boundary walks of the faces. Here, a pseudosurface is a topological space obtained from a closed surface (possibly disconnected) by identifying finitely many points.

The use of pseudosurfaces is very natural in this context: embeddings of different blocks can be glued together at their common cut-vertices. An example that pseudosurfaces are genuinely necessary is given below.

The bowtie graph, consisting of two triangles glued together at a single vertex. It has a unique cycle double cover. It contains each triangle twice. The corresponding embedding has four disc faces and lies naturally in two spheres identified at the common vertex. This shows that pseudosurfaces are genuinely necessary in the topological formulation of the problem.
The bowtie graph, consisting of two triangles glued together at a single vertex.
It has a unique cycle double cover. It contains each triangle twice.
The corresponding embedding has four disc faces and lies naturally in two spheres identified at the common vertex. This shows that pseudosurfaces are genuinely necessary in the topological formulation of the problem.

The algebraic counterpart of this topological statement is the following equivalent formulation: every bridgeless multigraph $G$ has a cycle double cover. That is, there exists a family $\{C_i\mid i\in I\}$ of cycles of $G$ such that every edge belongs to exactly two of the cycles $C_i$.

To see the connection, suppose first that such a cycle double cover is given. For every cycle $C_i$, take a disc and glue its boundary to the corresponding cycle in the graph. Since every edge occurs in exactly two cycles of the family, every edge is incident with two such discs. The resulting space is a pseudosurface in which the original graph is embedded and the added discs are precisely its faces.

For a simple example showing that pseudosurfaces are genuinely necessary in the above topological formulation of the cycle double cover conjecture, see the figure below.

Conversely, given such an embedding in a pseudosurface, the family $\{C_i\mid i\in I\}$ consists of the boundary walks $C_i$ of the faces of the embedding, which are cycles. Taken over all faces, these cycles form a cycle double cover, because every edge occurs exactly twice among the boundary walks of the faces.

The assumption that the graph is bridgeless is necessary. Indeed, a bridge is a cocircuit-singleton and thus cannot belong to any cycle and therefore cannot be covered even once by a cycle, let alone exactly twice.

About the proof

The proof by OpenAI establishes the second, algebraic formulation. In a nutshell, it begins with a nowhere-zero $\mathbb{F}_2^3$-flow $f$ on $G$; that is, an assignment of a nonzero vector in $\mathbb{F}_2^3$ to each edge such that, at every vertex, the values on the incident edges sum to zero. The existence of this flow follows from Seymour’s nowhere-zero six flow theorem (see also the recent short proof by DeVos and Nurse).

Roughly speaking, this flow is not quite a cycle double cover. The paper studies how one locally needs to modify the flow at each vertex so that it becomes a cycle double cover, and then there is a compatibility condition that needs to hold between adjacent vertices.

The compatibility conditions between the local modifications, and the equations for the local modifications give rise to a system of linear equations over $\mathbb{F}_2$, with one vector variable in $\mathbb{F}_2^3$ for each vertex and one scalar variable in $\mathbb{F}_2$ for each edge. OpenAI then uses duality to prove that this system always has a solution. The entire proof occupies only two pages.

Sang-il Oum gave an excellent talk on the proof and provides a much more detailed explanation. Jim Geelen (link) and Sang-il Oum (link) independently wrote short notes giving the complete proof in a different presentation, which I both find particularly pleasant to read and the latter additionally contains open questions.

Finally, the proof has already been formalised independently several times in Lean 4. Krystal Guo produced one formalisation of the core argument (personal communication), while Vaibhav Bajpai, Utku Okur, and I produced another, and one by OpenAI (see also this discussion in the AI-authored projects channel of the Lean Zulip community).

Matroid varieties

Posted on by
1

Universal models for graphic and representable matroids

Graphs have the useful property that each of them is a restriction of a complete graph on the same set of vertices. This property makes it easy, for example, to generate a random graph: simply flip a coin for each edge in the complete graph, and include the edge if the coin turns up heads. In matroidal terms, the property is that every rank-$n$ simple graphic matroid is a restriction of $M(K_{n+1})$.

There is another well known class of matroids for which a similar observation holds: those representable over a fixed finite field, in which case the projective geometry of a given rank serves as a “universal model”, in the sense that every simple rank-$n$ matroid that is representable over the finite field $\mathbb{F}_q$ can be obtained from $\text{PG}(n-1,\mathbb{F}_q)$ by restriction.

On the other hand, the same is not true for the class of all matroids. Even for matroids of rank 2, there is no universal model $M$ such that each such matroid is a restriction of $M$.

Dowling geometries

The class of graphic matroids is only one member of a family of classes with the same property: the Dowling matroids. These have been discussed before on the blog in the context of biased graphs, but let’s briefly recall their definition.

The rank-$n$ Dowling geometry $\text{DG}(n, \Gamma)$ is determined by a finite group $\Gamma$, similar to how projective geometries are determined by a field, and a Dowling matroid is simply any matroid that can be obtained by restricting $\text{DG}(n, \Gamma)$. Let’s assume that the operation in $\Gamma$ is multiplication. A $\Gamma$-gain graph is a graph $G$, together with an orientation of the edges of $G$ and a gain function $\varphi\colon E(G)\to\Gamma$. For a cycle $C$ of $G$, we pick a starting point an an orientation of $C$, which gives us an order of the edges of $C$, say $C = e_1e_2\ldots e_k$. Define $\varphi(C) = \varphi(e_1)^{s_1} \varphi(e_2)^{s_2} \ldots \varphi(e_k)^{s_k}$, where $s_i = 1$ if the orientation of $e_i$ agrees with the orientation of $C$, and $s_i = -1$ otherwise. The cycle $C$ is called “balanced” if $\varphi(C)$ is the identity in the group; it is a straightforward exercise to check that balance of $C$ does not depend on the orientation or starting point of $C$.

Two $\mathbb{Z}_3$-gain graphs. In the theta-graph on the left, all cycles are balanced; in the theta-graph on the right, only one cycle is balanced. Group elements are written additively.

A $\Gamma$-gain graph $G$ gives rise to a matroid on $E(G)$ whose circuits are the balanced cycles of $G$, as well as the theta-subgraphs with three unbalanced cycles, and subgraphs formed by two edge-disjoint unbalanced cycles connected by a (possibly empty) path that is disjoint from the two cycles except for its first and last vertex.

We can now define the Dowling geometry $\text{DG}(n,\Gamma)$ as the matroid obtained from the biased graph $K_n^\Gamma$ whose vertices are labelled $1, 2, \ldots, n$, which has one (unbalanced) loop attached at each vertex, and which has $|\Gamma|$ edges between vertices $i$ and $j$ (directed in towards the largest label, say), each labelled with a different group element.

If every (non-loop) edge is labelled by the identity in $\Gamma$, then every cycle is balanced. In particular, $\text{DG}(n,\langle 1\rangle) \cong M(K_{n+1})$, where we write $\langle 1\rangle$ for the trivial group. So, graphic matroids are Dowling matroids.

Varieties

Apart from graphic matroids, matroids representable over finite fields, and Dowling matroids, are there any other natural classes of matroids that have a sequence of universal models? It turns out that we have to be a bit careful with our definitions, but a beautiful result by Kahn and Kung from 1982 states that the answer is, essentially, no.

First, we need to define precisely what we mean by a universal model. Let $\mathcal{M}$ be a class of matroids. A sequence $M_1, M_2, M_3, \ldots$ of matroids is called a sequence of universal models for $\mathcal{M}$ if (i) for every $n$, $M_n$ is a rank-$n$ matroid, and (ii) for every $n$, every simple rank-$n$ matroid in $\mathcal{M}$ is isomorphic to a restriction of $M_n$. Thus, $\text{PG}(0,\mathbb{F}_q), \text{PG}(1,\mathbb{F}_q), \text{PG}(2, \mathbb{F}_q), \ldots$ is a sequence of universal models for the $\mathbb{F}_q$-representable matroids, and $\text{DG}(1,\Gamma), \text{DG}(2,\Gamma), \text{DG}(3,\Gamma), \ldots$ is a sequence of universal models for the Dowling matroids over the group $\Gamma$.

Second, we need to be careful about our definition of “natural” class of matroids. A class $\mathcal{M}$ is called a hereditary class if it is closed under isomorphism, as well as under taking minors and direct sums; so, if $M,N \in \mathcal{M}$ and $e$ is an element of $M$, then each of $M\backslash e$, $M/e$, and $M\oplus N$ are in $\mathcal{M}$ as well.

A variety of matroids is a hereditary class with a sequence of universal models. We are now ready to state Kahn and Kung’s result.

Theorem (Kahn–Kung, 1982). If $\mathcal{M}$ is a variety of matroids, then $\mathcal{M}$ is one of the following classes:

  • Matroids representable over a finite field;
  • Dowling matroids over a finite group; or
  • Matchstick geometries or Origami geometries.

The classes of matchstick and origami geometries have low connectivity. The universal models for matchstick geometries are $U_{2,n+1}^{\oplus k}$ and $U_{2,n+1}^{\oplus k} \oplus U_{1,1}$, depending on the parity of the rank, while the universal models for origami matroids are obtained from a basis ${b_1, …, b_r}$ by adding $n$ points freely to each of the lines spanned by pairs $\{b_i, b_{i+1}\}$.

Each of the assumptions (that the class of matroids be minor-closed, closed under direct sum, and have a sequence of universal models) in Kahn and Kung’s theorem is necessary for its conclusion. It is an amusing exercise to come up with classes of matroids that satisfy only a subset of these assumptions but not the others.