Stable matchings form a finite distributive lattice

Proved

StableMatching.stable_matchings_distribLattice

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

gale-shapleystable-matching

For every instance with $n$ men and $n$ women, there is a distributive lattice structure on the (finite) set of stable matchings whose order is: $\mu \le \nu$ iff every man $m$ weakly prefers $\mu(m)$ to $\nu(m)$ , i.e. $\mathrm{manRank}_m(\mu(m)) \le \mathrm{manRank}_m(\nu(m))$ for all $m$ .

Preamble

import Mathlib
import Definitions.Def_StableMatching_GaleShapley

Formal statement

namespace StableMatching

theorem stable_matchings_distribLattice {n : ℕ} (I : Instance n) :
    ∃ L : DistribLattice {μ : Matching n // I.IsStable μ},
      ∀ μ ν : {μ : Matching n // I.IsStable μ},
        L.le μ ν ↔ ∀ m : Fin n, I.manRank m (μ.1 m) ≤ I.manRank m (ν.1 m) := by sorry

end StableMatching

Source

Wikipedia, "Stable matching problem" (https://en.wikipedia.org/wiki/Stable_matching_problem), sections "Stable matching problem" (introduction), "Different stable matchings" and "Algorithmic solution"; primary reference: D. Gale, L. S. Shapley, College Admissions and the Stability of Marriage, Amer. Math. Monthly 69 (1962) 9–14, doi:10.2307/2312726.

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).
Endorsed by mikedeng1 · Nov 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph