Gale–Shapley is not truthful for women

Proved

StableMatching.galeShapley_not_truthful_women

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

gale-shapleystable-matching

There exist $n$ , instances $I$ and $I'$ with $n$ men and $n$ women, and a woman $w$ such that $I'$ differs from $I$ only in $w$ 's preference list and, with $\mu$ , $\mu'$ the Gale–Shapley outcomes of $I$ , $I'$ , woman $w$ strictly prefers (according to her true list in $I$ ) her partner $\mu'^{-1}(w)$ to $\mu^{-1}(w)$ .

Preamble

import Mathlib
import Definitions.Def_StableMatching_GaleShapley

Formal statement

namespace StableMatching

theorem galeShapley_not_truthful_women :
    ∃ (n : ℕ) (I I' : Instance n) (w : Fin n) (μ μ' : Matching n),
      I.WomanDeviation I' w ∧ I.IsGSOutcome μ ∧ I'.IsGSOutcome μ' ∧
      I.womanPrefers w (μ'.symm w) (μ.symm w) := 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