{"id":"palomar/PALOMAR-2026-10-29-000007","url":"https://github.com/jtraverso/corradi-hajnal/tree/2b85adcc37a9a057fb0cb72bc08774027f9ea077","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-29-000007-v1.json","repo":"https://github.com/jtraverso/corradi-hajnal","tags":["math.CO","msc:05C38","msc:05C70","msc:05C07"],"score":0,"title":"The Corrádi–Hajnal theorem on vertex-disjoint 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 the Corrádi–Hajnal theorem (1963): every finite simple graph on at least 3k vertices with minimum degree at least 2k contains k vertex-disjoint cycles. Cycles are closed walks that are cycles in Mathlib's sense; the theorem is also stated with the definition of disjoint cycles of the registered Erdős–Pósa entry (k pairwise disjoint vertex sets, each inducing a subgraph that is not acyclic). Both hypotheses are shown to be needed: for k ≥ 2 the complete graph on 3k − 1 vertices has minimum degree 3k − 2 ≥ 2k and no k disjoint cycles, and for m ≥ 2k the…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-29","reactions":{},"formalized":true,"formalizes":[{"title":"On the maximal number of independent circuits in a graph","identifier":"doi:10.1007/BF01895727","relationship":"formalizes"}]}