Gale–Shapley Theorem 1: existence of a stable complete matching

Proved

GS62CollegeAdmissions.paper_gs62_theorem1_stable_marriage_exists

by nkgarg · Sep 15, 2026 · Mathlib c5ea003 (Lean v4.30.0)

aml-gs62-stable-marriage-20260915game-theorystable-matching

Let $M$ and $W$ be equally sized finite sets. Each man strictly ranks all women, and each woman strictly ranks all men; everyone prefers any partner to being unmatched. Represent these rankings by real values $u_m(w)$ and $v_w(m)$ that are positive and have no ties within an individual's ranking. Then

\exists\mu:\quad \mu\text{ is a complete matching and has no blocking pair}.

A blocking pair consists of a man and a woman who both strictly prefer one another to their partners in $\mu$ . The matching assigns exactly one partner to each participant, with mutually consistent assignments. The empty market is included.

This is the stable-marriage existence result in Theorem 1 of Gale and Shapley's College Admissions and the Stability of Marriage.

Preamble

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Max
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Linarith
import Definitions.Def_AMLGS62_GS62CollegeAdmissions_MainTheorems

open GS62CollegeAdmissions
open AppliedModelingLib.Matching

Formal statement

theorem GS62CollegeAdmissions.paper_gs62_theorem1_stable_marriage_exists
    {M W : Type*} [Fintype M] [Fintype W] [DecidableEq M] [DecidableEq W]
    (val_m : M → W → ℝ) (val_w : W → M → ℝ)
    (hcard : Fintype.card M = Fintype.card W)
    (hdomain : gs_strict_marriage_domain val_m val_w) :
    ∃ mu : Assignment M W,
      gs_stable_marriage val_m val_w mu ∧ gs_complete_marriage mu := by sorry

Source

Gale and Shapley (1962), College Admissions and the Stability of Marriage, Theorem 1; https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/MainTheorems.lean#L94-L109

View graph