Mathlib3 PR that is worth rescuing?

Stream: mathlib4

[Weiyi Wang]

Occasionally I see people mention abandoned mathlib3 PR for theorems not yet formalized in mathlib4. I wonder how many there are? Is there a list of important mathlib3 PR that we'd like to get in mathlib4?

[Ruben Van de Velde]

I don't think anyone made a list

[Alex Meiburg]

There's Sperner's Lemma which would be nice to have. (And I'm not aware of anyone doing it in mathlib4)

[Junyan Xu]

If we are making a list here, I'd mention my coauthored PR mathlib3#18375 on path metric

[Yaël Dillies]

Alex Meiburg said:

There's Sperner's Lemma which would be nice to have. (And I'm not aware of anyone doing it in mathlib4)

Situation here is that I would be happy to supervise an undergrad to finish off the project

[Ruben Van de Velde]

I think you should file an issue about that

[Yaël Dillies]

#25231