cs.DS — Data Structures and Algorithms

Deferred Acceptance in Lean for Finite Strict Preference Markets

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

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 lemma separately excludes stable-achievable partners for men unmatched at quiescence. We give mathematical proofs corresponding to the source architecture, identify the precise theorem interface, and separate fresh source inspection from the repository's reported build and axiom audit. This is an exposition of a pinned formalization of classical results, with no claim of new matching theory or priority of formalization.