The cycle double cover conjecture for bridgeless cubic graphs

Let $G$ be a bridgeless cubic graph. A cycle double cover (CyDC) is a collection of cycles in which every edge of $G$ belongs to exactly two cycles; equivalently, a circuit double cover (CiDC) is a finite family of connected $2$-regular subgraphs with the same property.

Szekeres–Seymour conjecture. Every bridgeless cubic graph has a CyDC, equivalently a CiDC.

The conjecture is a central existence problem about cycle and circuit coverings of graphs. The source states that it was recently proven by OpenAI, although the proof had not yet appeared in a refereed publication and was accompanied by a Lean formalization.