[#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\).

Agent access

Work in ChatGPT

The agent reads this problem's research brief and asks you before it saves anything to TheoremDB.

Definitions and notation

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.

1Status

Saved packet · August 1, 2026

What counts as a solution

Saved packet status (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]

Reported answer models

GPT-5.6 Pro, OpenAIproof generationGPT-5.6 Sol, OpenAIwriteup

1Packet records

Show recorded summaries

Record	Kind	Assessment
The 2026 preprint reduces the graph problem to a four-colouring theorem for gaps of a cyclic word and derives a compatible circuit decomposition. Reported modelsGPT-5.6 Pro, OpenAI · GPT-5.6 Sol, OpenAI	Result	Claimed checked, not independently verifiednot Lean-verified
claim · Proposition 1 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] Relevance to this problem This is the source author's claimed resolution of the canonical conjecture, currently awaiting independent external review. Reported models GPT-5.6 Pro, OpenAIproof generationGPT-5.6 Sol, OpenAIwriteup Evidence Review pendingA complete argument is recorded and awaits independent review. Scope all finite connected Eulerian multigraphs with minimum degree at least four, including loops and parallel edges, with a specified Euler tour Sources Reference 1 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. Open full record →
A public Lean 4.31.0 development proves the compatibility endpoint and records a clean upstream audit; controlled TheoremDB verification is still pending.	Lean	Verification pending
formalization · Formalization 1 A public Lean 4.31.0 development proves the compatibility endpoint and records a clean upstream audit; controlled TheoremDB verification is still pending.^[2] Relevance to this problem This is a complete public formal proof of the packet's compatibility target in a pinned Lean world, awaiting replay by TheoremDB's verifier. Evidence Verification pendingAn accepted draft was submitted to the pinned verifier. A signed result is pending. Record state pending verification Scope the circuit-decomposition consequence for the finite endpoint multigraph model represented by Sabidussi.LoopMultigraph Sources Reference 2 Run `lake build && lake env lean Sabidussi/Audit.lean` Entry point `Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary` Runtime Lean 4.31.0 with mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8 Lean target draft lean target draft `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` Details The endpoint `Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary` takes an explicit Euler tour and a minimum-degree-four hypothesis, then produces an ordinary circuit decomposition compatible with that tour. Its graph model includes loops and parallel edges. The repository's production-source scan excludes `Challenge.lean`, which intentionally contains the statement placeholder used by Comparator. The production modules report no `sorry` or `admit`, and the upstream audit records only `propext`, `Classical.choice`, and `Quot.sound`. A separate Comparator workflow checks the solution wrapper against the reviewed statement. TheoremDB has pinned these materials but has not executed them inside its own controlled verifier. Related: Proposition 1 Open full record →
No records match these filters.

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

The overview places each record once. The relation list includes shared dependencies and names both ends of each link.

ProblemSabidussi's Compatibility Conjecture

All 1 recorded relations between these records and the problem

Pinned Lean proof in sabidussi-lean formalizes A compatible circuit decomposition is claimed for every eligible Euler tour

2See also

A period-six recurrence for domination on the three-row knight graphgraph theory
Leaf complexity of six-vertex graph connectivitygraph theory
Exact Hamiltonicity probability on eight labeled verticesgraph theory

Contribute to this problem

Cite this problem statement

Cite the original sources separately.

Plain text

“Sabidussi's Compatibility Conjecture.” TheoremDB. P3064. Problem statement; statement text SHA-256 23836014e98110010fefa22523196be4bba39e4e249f76d2a99c99a125c8ea74. https://theoremdb.org/statement/?ref=P3064

BibTeX

@misc{theoremdb-problem-23836014e98110010fefa22523196be4bba39e4e249f76d2a99c99a125c8ea74,
  title = {{Sabidussi's Compatibility Conjecture}},
  howpublished = {TheoremDB},
  note = {Problem statement; statement text SHA-256 23836014e98110010fefa22523196be4bba39e4e249f76d2a99c99a125c8ea74},
  url = {https://theoremdb.org/statement/?ref=P3064}
}

Plain text: Built Markdown snapshot

This problem includes 2 records joined by 1 typed links, sourced from arxiv.org^[1], current as of August 1, 2026.

1Lean verification

What the formal work covers

Formal statement

Pinned Lean proof in sabidussi-lean

Linked target: A compatible circuit decomposition is claimed for every eligible Euler tour

Target correspondence unavailable

the circuit-decomposition consequence for the finite endpoint multigraph model represented by Sabidussi.LoopMultigraph

This record has no accepted signed verification.

Assumptions and verification details

Recorded scope kind: universal

Inspect the full declaration and its assumptions in the formalization record.

Proof dependencies and replay

Lean blueprint

The source contains no sorries under Lean 4.31.0 with mathlib 9a9483a9. Signed verification is pending.

Check pending

Theorem

Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary

Pinned Lean proof in sabidussi-lean

Fully formalized

Lean 4 · read only

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

Theorem or lemma

Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary

Pinned Lean proof in sabidussi-lean

Fully formalized

lean-4.31.0/mathlib4@9a9483a92959bc92bd6a60176dd1fe597298c1f8+sabidussi-lean@da2f6ff7a7c7cc04e9ad34a53c3b6b8a18bd9ffa

Lean 4 · read only

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

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.

[#P3064] Sabidussi's Compatibility Conjecture

1Context

2Problem setup

3What counts as a solution

1Status

1Packet records

Recent contributions

2See also

1Lean verification

What the formal work covers

Formal statement

Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary

Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary

1References

Discussion

Report comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Record & provenance

Flag this problem

Sign in to follow

Report a problem

1Context

2Problem setup

3What counts as a solution

1Status

1Packet records

Recent contributions

2See also

1Lean verification

What the formal work covers

Formal statement

Sabidussi.LoopMultigraph.loop_sabidussi_compatibility_ordinary

1References

Add a comment

Background

Definitions

What counts as a solution

What's known

Formal statement

Recorded work

Related work

Record & provenance