Hall's marriage problem

Stream: graph theory

[Mario Krenn]

In the latest Lean blog (https://xenaproject.wordpress.com/2021/01/09/the-end-of-the-summer/), it's written that the Hall’s Marriage Theorem has been formalized. Unfortuantly there is no link somewhere. Could you please help me finding it?

Also it's mentioned "Alena gave a talk on that at Lean Together 2021", are there any recordings about this?

[Bryan Gin-ge Chen]

You can find a link to Alena's talk and slides here, see Thursday's talks.

[Bryan Gin-ge Chen]

They wrote up a preprint which you can find here and the code is in branch#simple_graph_matching.

[Mario Krenn]

Thanks a lot, remarkable!

[Kevin Buzzard]

I think that what is remarkable is not that Hall's marriage problem has been formalised. What is remarkable is that someone like @Alena Gusakov , who had never used Lean before the summer, can get good enough at it within a few months to knock off a 3rd year undergraduate theorem. Thanks Bryan for the links! I'll add them to the blog post.

[Kevin Buzzard]

For me this is what distinguishes Lean from the other provers. When you look at Freek's list, the people proving the theorems in the other provers tend to be the experts. With Lean they are sometimes people who have just learnt how to use the system, know the maths, and have made their way through the proof because at the end of the day Lean is not hard to learn, given the resources which we now have (e.g. this Zulip!)