Market Design

Definition Gale-Shapley Deferred Acceptance Algorithm formalized

Theorem Gale-Shapley Theorem (Existence of Stable Matching) proved

Theorem Lattice Structure of Stable Matchings (Conway-Knuth) proved

Definition Matching (Partial Bijection) formalized

Definition Matching Market (One-to-One) formalized

Theorem Proposing-Side Optimal Stable Matching proved

Theorem Rural Hospitals Theorem proved

Definition Stability (Individual Rationality + No Blocking Pair) formalized

Theorem Strategy-Proofness of Gale-Shapley for the Proposing Side (Roth 1982) staged