{"id":"palomar/PALOMAR-2026-08-27-000012","url":"https://github.com/sneed-and-feed/lean-theorems-1/tree/4aed8276b644003f18386038594b70de666938c2","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000012-v1.json","repo":"https://github.com/sneed-and-feed/lean-theorems-1","tags":["math.CO","msc:05A05","msc:05C70","msc:05D15","combinatorics","lean","hall-theorem","formal-verification"],"score":0,"title":"sneed-and-feed/lean-theorems-1","trust":"high","domain":"math.CO","source":"palomar","authors":["Sneed & Feed Formalization Team"],"reviews":0,"subject":"math.CO","summary":"A complete, machine-checked Lean 4 formalization of Hall's Marriage Theorem (Philip Hall 1935, Halmos–Vaughan 1950; Freek Wiedijk #87). Proves that an indexed family of finite sets admits a system of distinct representatives (SDR) if and only if Hall's marriage condition holds. 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-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"On Representatives of Subsets","identifier":"","relationship":"formalizes"},{"title":"The Marriage Problem","identifier":"","relationship":"adapts"}]}