Gale–Shapley Theorem 2: applicant-optimal college admissions

Proved

GS62CollegeAdmissions.PaperInterface.theorem2_applicant_optimality

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

aml-gs62-stable-marriage-20260915college-admissionsgame-theorystable-matching

Let $A,C$ be finite sets with decidable equality and let colleges have arbitrary quotas $q:C\to\mathbb N$ . Each participant strictly ranks potential partners and the outside option: real values are injective within each ranking and nonzero, with positive values for acceptable partners and outside-option value zero. Let $\mu^*$ be the assignment returned by the simultaneous waiting-list procedure from empty application histories.

For every stable assignment $\nu$ in the same market,

\forall a\in A,\qquad U_a(\nu(a))\le U_a(\mu^*(a)),\qquad U_a(\bot)=0.

Stable assignments respect quotas, are individually rational and have no replacement or acceptable-vacancy block. This theorem states the comparison inequality. The separate Section 4 theorem verifies termination and stability of $\mu^*$ . Empty markets, zero quotas, unmatched applicants and unfilled seats are allowed.

Preamble

import Mathlib.Algebra.BigOperators.Ring.Finset
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Fin.VecNotation
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Finset.Card
import Mathlib.Data.Finset.Lattice.Basic
import Mathlib.Data.Finset.Max
import Mathlib.Data.Finset.Sort
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Fintype.EquivFin
import Mathlib.Data.Fintype.Option
import Mathlib.Data.Fintype.Perm
import Mathlib.Data.Fintype.Sigma
import Mathlib.Data.Fintype.Sort
import Mathlib.Data.Prod.Lex
import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import Mathlib.Tactic.FinCases
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Ring
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_Basic
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_DeferredAcceptance
import Definitions.Def_AMLGS62_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62_GS62CollegeAdmissions_MainTheorems
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Foundations_Math_FiniteChoice
import Definitions.Def_AMLGS62Rest_AppliedModelingLib_Markets_Matching_ManyToOne
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_ExactCollegeBatchedProcedure
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_PaperInterface
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_SourceCompletion
import Definitions.Def_AMLGS62Rest_GS62CollegeAdmissions_SourceModel

open GS62CollegeAdmissions
open GS62CollegeAdmissions.PaperInterface

open AppliedModelingLib.Matching

Formal statement

theorem GS62CollegeAdmissions.PaperInterface.theorem2_applicant_optimality :
    theorem2_applicant_optimalitySpec := by sorry

Source

https://github.com/nikhgarg/AppliedModelingLib/blob/e952266be81e96bbeecea6af83d639af324a4438/papers/GS62CollegeAdmissions/ProofInterface.lean#L80-L94

View graph