Existence of stable matchings

Proved

StableMatching.stable_matching_exists

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

gale-shapleystable-matching

For every instance with $n$ men and $n$ women, each ranking all members of the other side strictly, there exists a stable matching: a bijection $\mu$ from men to women with no pair $(m,w)$ such that $m$ prefers $w$ to $\mu(m)$ and $w$ prefers $m$ to $\mu^{-1}(w)$ .

Preamble

import Mathlib
import Definitions.Def_StableMatching_GaleShapley

Formal statement

namespace StableMatching

theorem stable_matching_exists {n : ℕ} (I : Instance n) :
    ∃ μ : Matching n, I.IsStable μ := 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