[#P3064] Sabidussi's Compatibility Conjecture
Problem. Let \(G\) be a finite connected Eulerian multigraph with minimum degree at least \(4\), with loops and parallel edges allowed, and let \(T\) be an Euler tour of \(G\). Prove that the labelled edges of \(G\) can be partitioned into circuits so that no circuit contains two edges consecutive in the cyclic order of \(T\).
1Context
The Euler tour fixes a cyclic transition at each passage through a vertex. A compatible decomposition asks that each circuit avoid every transition prescribed by that tour.
2Problem setup
Definition 1 (Compatible circuit decomposition). A partition of all labelled edges into circuits in which no circuit uses either edge pair from a transition induced by the Euler tour.
Convention 1. The cyclic transition from the last tour edge to the first is included. Loops and parallel edges are allowed.
3What counts as a solution
- Produce a partition of all labelled edges into connected 2-regular circuits, using every edge exactly once, such that every cyclic pair of consecutive tour edges belongs to different circuits.
- A formal certificate must cover loops, parallel edges, the closing tour transition, the minimum-degree hypothesis, and the circuit-decomposition conclusion.
1StatusProof claimednot Lean-verified
Claimed answer (A compatible circuit decomposition is claimed for every eligible Euler tour). The 2026 preprint reduces the graph problem to a four-colouring theorem for gaps of a cyclic word and derives a compatible circuit decomposition.[1]
Resolution argument
Orient every edge in the direction of the given Euler tour and record the vertex at each passage. The resulting cyclic word contains each vertex degree divided by two times, hence at least twice. The paper's central cyclic-word theorem colours the gaps by the four elements of F_2 squared. Adjacent gaps receive different colours, and at each letter every colour occurs an even number of times among the two gap incidences at its occurrences.
Transfer each gap colour to the corresponding tour edge. Different colours on adjacent gaps mean that the two edges in every tour transition have different colours, including the transition between the final and first edges. The even-incidence condition says that each colour class induces an even subgraph at every vertex. Every finite even multigraph splits into connected 2-regular circuits by taking an Euler tour in each nonempty component and splitting closed trails at repeated vertices. Apply this decomposition separately to the four colour classes. The resulting circuits partition all edges, and no circuit can contain both edges of a prescribed transition because each circuit is monochromatic while every transition has two colours.
The cyclic-word theorem is proved with two parity lemmas over F_2. Passing from gap colours to their nonzero successive differences gives three possible local zero-sum patterns at each letter. A global balancing lemma selects one pattern per letter so that the remaining quadratic parity conditions vanish, after which prefix sums recover the required gap colours. This establishes the stronger four-colouring statement and the stated circuit consequence. Independent external mathematical review of this new proof was not identified in the dated search, so TheoremDB presents it as review pending.
1Records
Notes and companion material
Original intake status. CLAIMED RESOLVED in arXiv:2607.13225v1, posted July 14, 2026. The author supplies a public Lean formalization. Independent external mathematical review was not identified as of 2026-08-01.
- The paper attributes the conjecture to Gert Sabidussi and says Herbert Fleischner recorded it.
- The paper says GPT-5.6 Pro generated the proof and GPT-5.6 Sol helped with the writeup. Nikolay Ulyanov authored the paper and Lean project.
- The public Lean endpoint proves the compatibility consequence for the loop-and-parallel-edge model. The paper's stronger four-colouring statement is outside this entry's target.
- Challenge.lean contains an intentional statement placeholder and is excluded from the production source scan. The production modules report no sorry or admit. TheoremDB has not yet rerun the source in its controlled verifier.
How the 2 records connect
ProblemSabidussi's Compatibility Conjecture
2See also
- Cycle Double Cover Conjecturegraph theory
- Is there a truly subcubic algorithm for weighted APSP?graph theory
- The Total Coloring Conjecturegraph theory
How to cite
TheoremDB contributors, “Sabidussi's Compatibility Conjecture,” TheoremDB research memory, snapshot of August 1, 2026. https://theoremdb.org/statements/sabidussi-compatibility-conjectureThis page as plain text: sabidussi-compatibility-conjecture.md
This problem includes 2 records joined by 1 typed links, sourced from arxiv.org[1], current as of August 1, 2026.
1Lean verification
Lean blueprint
The source contains no sorries under Lean 4.31.0 with mathlib 9a9483a9. Signed verification is pending.
Theorem
Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary
Pinned Lean proof in sabidussi-lean
Fully formalized
theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary
{G : LoopMultigraph V E} (T : G.EulerTour)
(hmin : ∀ v : V, 4 ≤ G.degree v) :
∃ S : G.OrdinaryCircuitDecomposition, S.Compatible T- World
- lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+sabidussi-lean@da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa
- Kernel
- Pending
Finish Lean verification
Lean work is attached and awaits signed verification. TheoremDB Researcher can continue from the current declarations and pinned world.
Continue in TheoremDB ResearcherThe prefilled request prepares the exact target and checks the current work. It submits an accepted proof and polls verification through any packet-review handoff.
1References
- Packet source. Nikolay Ulyanov, Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture, arXiv:2607.13225v1 (2026). Abstract; Section 1; Theorem 1.1; Statement of AI use. ↗preprint · primary source · v1 · checked 2026-08-01Source use: original summary.States a stronger four-colouring theorem, derives the compatibility conjecture, and records that GPT-5.6 Pro generated the proof with GPT-5.6 Sol assisting the writeup.Also cited at Abstract; Section 1 definitions, Theorem 1.1, attribution, Statement of AI use, and acknowledgements.Also cited at Abstract; Section 1; Theorem 1.1; Statement of AI use; acknowledgements.Also cited at Abstract and Sections 1-4, especially Theorems 1.1 and 2.1.Source used to formulate or check the problem record.States a stronger four-colouring theorem, derives the compatibility conjecture, records that GPT-5.6 Pro generated the proof with GPT-5.6 Sol assisting the writeup, and thanks Tom de Groot for exposition suggestions.Source named by the research packet.
- Nikolay Ulyanov, sabidussi-lean, commit da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa (2026). Sabidussi/OrdinaryCircuit.lean, theorem loop_sabidussi_compatibility_ordinary; formalization.yaml; VERIFICATION.md. ↗software · software source · da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa · checked 2026-08-01Source use: citation only.Pinned Lean 4.31.0 formalization of the circuit-decomposition consequence and upstream verification record.Also cited at Sabidussi/OrdinaryCircuit.lean theorem Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary and VERIFICATION.md.
- Herbert Fleischner, Eulersche Linien und Kreisüberdeckungen, die vorgegebene Durchgänge in den Kanten vermeiden, Journal of Combinatorial Theory, Series B 29(2) (1980), 145-167. Original recording; attribution cross-checked in Ulyanov, Section 1. ↗journal article · reference sourceSource use: original summary.Records the conjecture attributed to Gert Sabidussi and proves the planar case.
Original CC0 restatement prepared by TheoremDB after checking the preprint and pinned Lean repository.