Berge's theorem, the Tutte–Berge formula and the Gallai–Edmonds theorem
A Lean 4 / Mathlib formalization of Berge's augmenting path theorem (a matching is maximum if and only if there is no augmenting path) and of the Tutte–Berge formula (the maximum size of a matching is the minimum over vertex sets U of (|V| + |U| − odd(G − U)) / 2), with the weak inequality for all matchings and vertex sets; the formula is derived from Mathlib's Tutte theorem by adding universal vertices. Version 2 adds the Gallai–Edmonds structure theorem: with D the vertices missed by some maximum matching, A their neighbours outside D and C the rest, the components of G[D] are…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-10-16-000011
curl -X POST /api/v1/records/palomar/PALOMAR-2026-10-16-000011/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-000011/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'