{"id":"palomar/PALOMAR-2026-08-17-000003","url":"https://github.com/gexahedron/sabidussi-lean/tree/58307d74da99ec6e4fe28e012c30c83e369c54c3","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-17-000003-v1.json","repo":"https://github.com/gexahedron/sabidussi-lean","tags":["math.CO","msc:05C45","msc:05C70","graph-theory","lean-formalization"],"score":0,"title":"gexahedron/sabidussi-lean","trust":"high","domain":"math.CO","source":"palomar","authors":["Nikolay Ulyanov"],"reviews":0,"subject":"math.CO","summary":"Sabidussi compatibility in Lean","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-17","reactions":{},"formalized":true,"formalizes":[{"title":"Graph Puzzles III.1: A Proof of Sabidussi's Compatibility Conjecture","identifier":"https://arxiv.org/abs/2607.13225","relationship":"formalizes"}]}