Sabidussi's compatibility conjecture proved
The edges of a finite connected multigraph carrying a closed eulerian trail can be partitioned into circuits so that no circuit contains two edges used consecutively in the trail, with a Lean 4 formalization.
- Lab
- Independent
- Model
- GPT-5.6 Pro, GPT-5.6 Sol
- Field
- Mathematics
- Date
- 2026-07-14
- Human collaborators
- Nikolay Ulyanov
Sources
Original work
Independent commentary
What was found
Sabidussi's conjecture asks whether, given a finite connected multigraph together with a closed eulerian trail, the edge set can always be partitioned into circuits none of which contains two edges that the trail uses consecutively. The proof establishes this and in fact does more: it four-colours the edges so as to satisfy the constraints. The work was developed with GPT-5.6 Pro and GPT-5.6 Sol, with the author reviewing the proof, and a Lean 4 formalization accompanies the preprint in the author's repository.
Novelty check
Sabidussi's compatibility conjecture is a named open problem in graph theory concerning eulerian trails and compatible circuit decompositions, with a partial-results literature covering restricted degree conditions. It was recorded as open in the general case. No prior general proof appears.
Caveats and known objections
Not peer-reviewed. The Lean formalization is in the author's own repository and had no independent audit at announcement. Autonomy graded collaborative rather than ai-led: the source describes the proof as developed with the models and reviewed by the author, without attributing the key idea specifically to the model, so the weaker defensible reading applies.
Nobody outside the lab has checked this yet.
Reading the primary source closely enough to say whether it supports the claim counts as a check, and you are credited on the entry.
Or on GitHub: submit a check challenge the grade send a correction or send a pull request
Flag this for triage
Signals order the review queue and nothing else. They are never published, and they never move a grade: that takes a citation.
Entry history (1 event)
- AddedEntered the registry graded Formally verified and Collaborative.
Entries are never deleted. A grade that does not hold up is downgraded on the record, with the reason beside it.
Graded formally verified for verification and collaborative for autonomy. What these mean.
Cite this entry
whataifound.org. (2026). Sabidussi's compatibility conjecture proved. whataifound.org: A Registry of AI Scientific and Mathematical Discoveries. https://whataifound.org/finding/2026-07-14-sabidussi-compatibilityBibTeX
@misc{whataifound-independent-2026-compatibility,
title = {Sabidussi's compatibility conjecture proved},
author = {{whataifound.org}},
year = {2026},
howpublished = {whataifound.org: A Registry of AI Scientific and Mathematical Discoveries},
note = {Result by Independent. Verification: Formally verified. Autonomy: Collaborative.},
url = {https://whataifound.org/finding/2026-07-14-sabidussi-compatibility}
}