Gale–Shapley is group strategy-proof for men

Proved

StableMatching.galeShapley_group_strategyproof_men

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

gale-shapleystable-matching

Let $C$ be a nonempty set of men and let $I'$ be obtained from $I$ by changing only the preference lists of the men in $C$ . Let $\mu$ and $\mu'$ be the Gale–Shapley outcomes of $I$ and $I'$ . Then it is not the case that every man $m \in C$ strictly prefers, according to his true list in $I$ , $\mu'(m)$ to $\mu(m)$ .

Preamble

import Mathlib
import Definitions.Def_StableMatching_GaleShapley

Formal statement

namespace StableMatching

theorem galeShapley_group_strategyproof_men {n : ℕ} (I I' : Instance n) (C : Finset (Fin n))
    (hC : C.Nonempty) (hdev : I.MenDeviation I' C) (μ μ' : Matching n)
    (hμ : I.IsGSOutcome μ) (hμ' : I'.IsGSOutcome μ') :
    ¬ ∀ m ∈ C, I.manPrefers m (μ' m) (μ m) := 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