Open Research Index

sneed-and-feed/lean-theorems-1

Sneed & Feed Formalization Team

Palomar Registrypalomar/PALOMAR-2026-08-27-000012Aug 27, 2026math.COscore 0

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).

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-27-000012
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000012/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-08-27-000012/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'