Gale–Shapley outcome is woman-pessimal

Proved

StableMatching.galeShapley_woman_pessimal

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

gale-shapleystable-matching

Let $\mu_0$ be the Gale–Shapley outcome of an instance and let $\mu$ be any stable matching of the same instance. Then every woman $w$ weakly prefers her partner in $\mu$ to her Gale–Shapley partner: $\mathrm{womanRank}_w(\mu^{-1}(w)) \le \mathrm{womanRank}_w(\mu_0^{-1}(w))$ .

Preamble

import Mathlib
import Definitions.Def_StableMatching_GaleShapley

Formal statement

namespace StableMatching

theorem galeShapley_woman_pessimal {n : ℕ} (I : Instance n) (μ₀ μ : Matching n)
    (h₀ : I.IsGSOutcome μ₀) (hμ : I.IsStable μ) (w : Fin n) :
    I.womanRank w (μ.symm w) ≤ I.womanRank w (μ₀.symm w) := 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).

View graph