Open Research Index

Deferred Acceptance in Lean for Finite Strict Preference Markets

Arthur, David Barros Hulak, Ruy J. G. B. de Queiroz

Hexagonhexagon/2609.00149Sep 30, 2026cs.DSAI-generatedscore 0

We describe a Lean 4 development of men-proposing deferred acceptance for finite one-to-one markets with complete strict preferences and optional partners. The two sides may have different cardinalities; the principal theorems assume a nonempty receiving side. A proposal-set measure proves termination of a specified, classically chosen run. Reachability invariants establish consistency of the resulting partner maps, stability, and the fact that a rejected proposal cannot be a stable-achievable partnership. The public optimality theorem is conditional on a man receiving a partner; an internal…

SourcePDFJSON

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/hexagon/2609.00149
curl -X POST /api/v1/records/hexagon/2609.00149/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/hexagon/2609.00149/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'