{"id":"palomar/PALOMAR-2026-10-28-000010","url":"https://github.com/jtraverso/edmonds-matching-polytope/tree/6198b8314ac88a5638120fcf15d5b58c024caaab","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-28-000010-v1.json","repo":"https://github.com/jtraverso/edmonds-matching-polytope","tags":["math.CO","math.OC","msc:05C70","msc:90C27","msc:52B12"],"score":0,"title":"Edmonds' perfect matching polytope and matching polytope","trust":"high","domain":"math.CO","source":"palomar","authors":["Juan Pablo Traverso Gianini"],"reviews":0,"subject":"math.CO","summary":"A Lean 4 / Mathlib formalization of Edmonds' theorems (1965) for finite simple graphs: the convex hull of the incidence vectors of the perfect matchings is {x ≥ 0, x(δ(v)) = 1 for every vertex v, x(δ(S)) ≥ 1 for every odd set S}, and the convex hull of the incidence vectors of all matchings is {x ≥ 0, x(δ(v)) ≤ 1, x(E[S]) ≤ (|S| − 1)/2 for every odd S}. Vectors are indexed by the edges of the graph, the convex hull is Mathlib's convexHull, and matchings are Mathlib's Subgraph.IsMatching and Subgraph.IsPerfectMatching. The perfect matching theorem is proved for multigraphs by induction with…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-28","reactions":{},"formalized":true,"formalizes":[{"title":"Maximum matching and a polyhedron with 0,1-vertices","identifier":"doi:10.6028/jres.069B.013","relationship":"formalizes"}]}