{"id":"palomar/PALOMAR-2026-10-18-000001","url":"https://github.com/jtraverso/chvatal-posa-hamiltonian/tree/6be0ebda7b457b85ad400f6d7f92ad156d6e7712","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-18-000001-v1.json","repo":"https://github.com/jtraverso/chvatal-posa-hamiltonian","tags":["math.CO","msc:05C45","msc:05C07","hamiltonian-cycles","graph-theory","lean","degree-conditions"],"score":0,"title":"Chvátal's and Pósa's degree conditions for Hamiltonian cycles","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of two classical degree-sequence conditions for Hamiltonicity of a finite simple graph on n ≥ 3 vertices with degrees d₁ ≤ ⋯ ≤ dₙ. Chvátal's theorem (1972): if for every i < n/2, dᵢ ≤ i implies d_{n−i} ≥ n − i, then the graph is Hamiltonian (stated without sorting: if at least i vertices have degree at most i, then at least i + 1 vertices have degree at least n − i). Pósa's theorem (1962): if for every k with 1 ≤ k < (n − 1)/2 fewer than k vertices have degree at most k, and, for odd n, at most (n − 1)/2 vertices have degree at most (n − 1)/2, then the graph…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-18","reactions":{},"formalized":true,"formalizes":[{"title":"On Hamilton's ideals","identifier":"doi:10.1016/0095-8956(72)90020-2","relationship":"formalizes"},{"title":"A theorem concerning Hamilton lines","identifier":"","relationship":"formalizes"}]}