The Corrádi–Hajnal theorem on vertex-disjoint cycles
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-29-000007
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-29-000007/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-29-000007/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'