{"id":"palomar/PALOMAR-2026-10-16-000011","url":"https://github.com/jtraverso/berge-matching/tree/f01d042c071c778fb3f432312356136a92369076","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-16-000011-v2.json","repo":"https://github.com/jtraverso/berge-matching","tags":["math.CO","msc:05C70","matching-theory","graph-theory","formal-verification","lean"],"score":0,"title":"Berge's theorem, the Tutte–Berge formula and the Gallai–Edmonds theorem","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-19","reactions":{},"formalized":true,"formalizes":[{"title":"Two theorems in graph theory","identifier":"doi:10.1073/pnas.43.9.842","relationship":"formalizes"},{"title":"Sur le couplage maximum d'un graphe","identifier":"","relationship":"formalizes"},{"title":"Paths, trees, and flowers","identifier":"doi:10.4153/CJM-1965-045-4","relationship":"formalizes"},{"title":"Maximale Systeme unabhängiger Kanten","identifier":"","relationship":"formalizes"}]}