A male-optimal stable matching exists

Proved

AGT.male_optimal_exists

by Shuze Chen · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

game-theorymarket-designmechanism-designstable-matching

Some stable matching is weakly best for every man simultaneously — Gale–Shapley's optimal assignment (1962, Theorem 2). In every finite marriage market with strict preferences and $|M| = |W|$ there is a stable $\mu$ such that for every stable $\nu$ and every man $m$ , either $\mu(m) = \nu(m)$ or $m$ strictly prefers $\mu(m)$ to $\nu(m)$ .

A note on the rendering and the attribution. Theorem 10.11 of Algorithmic Game Theory states the male-optimality of the Deferred Acceptance outcome in the book's own, weaker form: no stable alternative makes every man weakly and some man strictly better off (p. 257). The man-by-man form asserted here is Gale–Shapley's original notion and implies the book's outright; conversely, for finite strict markets any Pareto-undominated stable matching coincides with the man-by-man optimum (which exists), so the two definitions carve out the same matchings — but that equivalence is a theorem, which is why this statement is attributed to Gale–Shapley 1962 and only rendered from the book's Theorem 10.11. With strict preferences the male-optimal stable matching is unique — two of them would be weakly preferred to each other by every man — which is what lets the capstone speak of the male-optimal mechanism. This statement is deliberately freed of the algorithm; any construction of Deferred Acceptance proves it.

Preamble

import Definitions.Def_agt_matching

Formal statement

namespace AGT

/-- A male-optimal stable matching exists: there is a stable matching that
every man weakly prefers to every other stable matching — the male-propose
Deferred Acceptance outcome.  The man-by-man form of optimality asserted
here is Gale–Shapley's (1962, Theorem 2); Theorem 10.11 of *Algorithmic
Game Theory* states the equivalent no-Pareto-improvement form — no stable
alternative makes every man weakly and some man strictly better off —
which this statement implies outright and, for finite strict markets,
also follows from (any Pareto-undominated stable matching coincides with
the man-by-man optimum). -/
theorem male_optimal_exists {M W : Type*} [Fintype M] [Fintype W]
    (PM : M → W → W → Prop) (PW : W → M → M → Prop)
    (hM : IsPrefProfile PM) (hW : IsPrefProfile PW)
    (hcard : Nonempty (M ≃ W)) :
    ∃ μ : M ≃ W, IsMaleOptimal PM PW μ := by
  sorry

end AGT

Source

D. Gale, L. S. Shapley, College admissions and the stability of marriage, Amer. Math. Monthly 69 (1962), Theorem 2, https://doi.org/10.2307/2312726; rendered from N. Nisan et al. (eds.), Algorithmic Game Theory, CUP 2007, Section 10.4.1, Theorem 10.11, p. 257 (the book states the equivalent no-Pareto-improvement form)

Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back: `male_optimal_exists`

Setting and hypotheses. Let $M$ and $W$ be two finite types (either or both may be empty). The data and hypotheses are exactly as in the companion existence statement:

$P^M$ assigns to each $m \in M$ a binary relation $P^M_m$ on $W$ ; $P^W$ assigns to each $w \in W$ a binary relation $P^W_w$ on $M$ (write $P^M_m(w,w')$ , resp. $P^W_w(m,m')$ , when the relation holds of that ordered pair);
$h_M$ : every $P^M_m$ is a strict total order on $W$ (trichotomous, irreflexive, transitive); $h_W$ : every $P^W_w$ is a strict total order on $M$ ;
$h_{\mathrm{card}}$ : the type of bijections $M \simeq W$ is nonempty — some bijection between $M$ and $W$ merely exists (with finiteness, equivalently $|M| = |W|$ ).

Conclusion. There exists a bijection $\mu : M \to W$ (an Equiv, i.e. a map with two-sided inverse $\mu^{-1}$ ) satisfying the conjunction of the following two clauses (this unfolds the custom predicate IsMaleOptimal):

$\mu$ is a stable matching (unfolding IsStableMatching/IsBlockingPair): no pair blocks it,

\forall m \in M,\ \forall w \in W:\quad \neg\Big( P^M_m\big(w,\ \mu(m)\big) \ \wedge\ P^W_w\big(m,\ \mu^{-1}(w)\big) \Big);

man-by-man weak dominance over every stable matching: for every bijection $\nu : M \to W$ that is itself a stable matching in the same sense, and for every man $m \in M$ ,

\mu(m) = \nu(m) \quad \text{or} \quad P^M_m\big(\mu(m),\ \nu(m)\big),

i.e. $m$ 's partner under $\mu$ equals his partner under $\nu$ , or $m$ 's relation holds of the ordered pair ( $\mu$ 's assignment, $\nu$ 's assignment).

Remarks on scope and edge cases. Clause 2 quantifies over all stable bijections $\nu$ , including $\nu = \mu$ (where the first disjunct is trivial). No condition of any kind is imposed on the women's side beyond stability — there is no claim of woman-pessimality. The theorem asserts mere existence ( $\exists$ , not $\exists!$ ); it does not assert uniqueness of a male-optimal matching, nor name a construction. If $M$ and $W$ are both empty, the empty bijection witnesses the claim vacuously; if exactly one of them is empty, $h_{\mathrm{card}}$ fails and the statement is vacuously true.

Human review

Endorsed by Community (Bot) · Sep 13, 2026
Endorsed by Shuze Chen · Sep 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

A male-optimal stable matching exists

Read-back: male_optimal_exists

Read-back: `male_optimal_exists`