The 3×3 example has exactly three stable matchings

Proved

StableMatching.example3_stable_iff

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

gale-shapleystable-matching

For the instance with men $A,B,C$ and women $X,Y,Z$ and preferences $A: YXZ$ , $B: ZYX$ , $C: XZY$ , $X: BAC$ , $Y: CBA$ , $Z: ACB$ , a matching is stable if and only if it is one of $(AY, BZ, CX)$ , $(AX, BY, CZ)$ , $(AZ, BX, CY)$ .

Preamble

import Mathlib
import Definitions.Def_StableMatching_GaleShapley

Formal statement

namespace StableMatching

theorem example3_stable_iff (μ : Matching 3) :
    example3.IsStable μ ↔
      (⇑μ = ![1, 2, 0] ∨ ⇑μ = ![0, 1, 2] ∨ ⇑μ = ![2, 0, 1]) := 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