{"id":"palomar/PALOMAR-2026-09-02-000010","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/87f8794c71218c0174f51248bde1396f3793abdd","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-02-000010-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05C70","msc:05C69","msc:90C27","graph-theory","matchings","lean-formalization"],"score":0,"title":"The Kőnig–Egerváry Theorem on Matchings and Vertex Covers in Bipartite Graphs","trust":"high","domain":"math.CO","source":"palomar","authors":["Noah Cohen"],"reviews":0,"subject":"math.CO","summary":"A complete machine-checked Lean 4 formalization of the Kőnig–Egerváry Theorem (1931) and Gallai identities (1959). Proves strong min-max duality matchingNumber(G) = vertexCoverNumber(G) for 2-colorable graphs G via Hall's defect matching theorem, and formalizes Gallai's identity independenceNumber(G) + vertexCoverNumber(G) = |V(G)|. To the maintainers' knowledge, the theorem was not found in an exact declaration name, docstring, and type signature search of the pinned Mathlib revision (Mathlib v4.34.0-rc1).","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-02","reactions":{},"formalized":true,"formalizes":[{"title":"Gráfok és mátrixok","identifier":"","relationship":"formalizes"},{"title":"Matrixok kombinatorius tulajdonságairól","identifier":"","relationship":"formalizes"},{"title":"Über extreme Punkt- und Kantenmengen","identifier":"","relationship":"adapts"},{"title":"On Representatives of Subsets","identifier":"","relationship":"adapts"}]}