Mader's theorem and Hadwiger's conjecture for t ≤ 4
Source: github.com/jtraverso/hadwiger-mader/tree/a1ffd32233475c21ad…
A Lean 4 / Mathlib formalization of Mader's theorem (a nonempty finite graph of average degree at least 2^(r−2) has a K_r minor), of Dirac's lemma (a graph without a K4 minor has a vertex of degree at most two, hence at most 2n − 3 edges for n ≥ 2), of Mader's bound for K5 (a graph on n ≥ 3 vertices with at least 3n − 5 edges has a K5 minor; equivalently, without a K5 minor it has at most 3n − 6 edges; added in version 2), and of Hadwiger's conjecture for t ≤ 4 (graphs without a K3 minor are 2-colourable, graphs without a K4 minor are 3-colourable). Minors are branch-set models.
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-16-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000001/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-16-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'