Gale-Shapley algorithm formalization

Stream: maths

[Ted Hwa]

I have formalized some results In Lean about stable matchings and the Gale-Shapley algorithm at this repo. It has the basic results (the algorithm produces a stable matching, and it is proposer optimal), as well as some more advanced results found in Dumont's paper (in French).

This is an unusual (?) case where the foundations of the theory depend on an algorithm. Indeed, I don't know of any other way to show that a stable matching always exists. So proving the results required implementing the algorithm in Lean and proving invariants about it. Then I had to develop some utilities to be able to study an algorithm step by step. I needed to be able to write lemmas that say, if the algorithm reaches some state, then some other state happens next, or has happened sometime earlier, or will happen sometime later. I couldn't find any existing such tools in Mathlib.

The basic version of the algorithm uses choose to achieve maximum generality in the proofs, but I also included a computable version of the algorithm that can run in Lean. I actually made 2 implementations of computable versions, but one of them is very slow at a small case (n=4) for reasons I don't fully understand yet.

Is this worth PR to mathlib? How much more work would it be?

[Yaël Dillies]

Nice job! This is definitely worth including in mathlib, although I can't tell you how much work it would be without seeing your code

[Ted Hwa]

The code is at https://github.com/hwatheod/galeshapley-lean

[Yaël Dillies]

Okay, it will take... a while :upside_down:

[Yaël Dillies]

But you can certainly try! Learn by doing, as they say. And if you get bored of PRing, one of us can take over.

[Ruben Van de Velde]

Put it on a wiki :)

[Richard Osborn]

Perhaps the computational component can be PRd to Batteries first? (or in parallel)

[Shreyas Srinivas]

Why batteries? Gale Shapley is a strictly mathematical theoretical result

[Ruben Van de Velde]

It's even harder to get reviews in batteries than mathlib. I recommend to stick to mathlib

[Shreyas Srinivas]

Further I don't see any computational benefit for the typical programmer from an implementation of Gale Shapley. Batteries is to Lean what boost is to C++.

[Mario Carneiro]

Yes, this does not sound suitable for batteries in its current state. Algorithms in batteries are meant to be run first and proved second

[Mario Carneiro]

Ruben Van de Velde said:

It's even harder to get reviews in batteries than mathlib. I recommend to stick to mathlib

This is also very true. It's much easier to review something for batteries that has already gone through mathlib's review process, plus there is some order of magnitude more eyeballs in general in the mathlib queue (although t-meta PRs are still pretty slow, since all the mathlib meta reviewers got hired away...)