Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture

Nikolay Ulyanov

Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture

Combinatorics 2026-07-14 v1

Authors: Nikolay Ulyanov

Abstract

We prove Sabidussi's compatibility conjecture. Let $G$ be a finite connected multigraph in which every vertex has even degree and the minimum degree is at least four, and let $T$ be a closed trail that traverses every edge exactly once. The edges of $G$ can be partitioned into circuits (connected 2-regular subgraphs) so that no circuit contains the two edges used consecutively anywhere in $T$ . In fact, the edges can be four-coloured so that every such pair receives two different colours and the subgraph formed by the edges of each colour has even degree at every vertex. Formalization in Lean 4 is also available in the author's github.

Keywords

Sabidussi's conjecture compatibility closed trails circuits graph coloring

Cite

@article{arxiv.2607.13225,
  title  = {Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture},
  author = {Nikolay Ulyanov},
  journal= {arXiv preprint arXiv:2607.13225},
  year   = {2026}
}