{"id":"palomar/PALOMAR-2026-10-18-000011","url":"https://github.com/jtraverso/dirac-common-cycle/tree/3c9e9966662cb99c0e4f11d771011bc904dc627f","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000011-v1.json","repo":"https://github.com/jtraverso/dirac-common-cycle","tags":["math.CO","msc:05C38","msc:05C40","graph-theory","k-connected-graphs","lean","cycles"],"score":0,"title":"Dirac's theorem: k vertices of a k-connected graph lie on a common cycle","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Dirac's 1960 theorem: in a k-connected finite simple graph with k ≥ 2 (more than k vertices, and connected after deleting any set of fewer than k vertices), any set of at most k vertices lies on a common cycle. In particular, in a 2-connected finite graph any two vertices lie on a common cycle. Cycles are Mathlib's `SimpleGraph.Walk.IsCycle`. Mathlib does not have this theorem.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"In abstrakten Graphen vorhandene vollständige 4-Graphen und ihre Unterteilungen","identifier":"doi:10.1002/mana.19600220107","relationship":"formalizes"}]}