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
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.
Machine-checked elsewhere
PalomarPALOMAR-2026-08-17-000003
gexahedron/sabidussi-lean at 58307d74da99 · checked 2026-08-17
Provedsabidussi_compatibility_ordinary
A Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
Palomar's record does not restate the theorem in prose, so what the registration certifies is that formal statement rather than the preprint's phrasing of it.
The open problem
MathDBSabidussi's compatibility conjecture
388102
Nothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
A bare problem record: MathDB has no progress summary and no solution posted for it, so this places the problem in that catalogue rather than corroborating the resolution.
Also recorded at
vibemathedSabidussi's Compatibility Conjecture
sabidussi-compatibility
Nothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.
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.
History of this entry
- CorrectedRecorded the MathDB problem record as a third registration, alongside Palomar and vibemathed. The page carries nothing about the resolution, so no grade moved.
- CorrectedRecorded the vibemathed record for this result as a registration. The vibemathed link it replaces pointed at that site's home page rather than at this result, and was classified as commentary, which a registry listing is not.
- CheckedPalomar registered the author's Lean development as PALOMAR-2026-08-17-000003, so the formalization now carries the mechanical audit it did not have at announcement. The repository was also added as a source: the entry had linked no artifact at all. source ↗
- 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}
}