Zulip Chat Archive

Stream: graph theory

Topic: Hall's marriage problem


Mario Krenn (Jan 10 2021 at 00:27):

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 (Jan 10 2021 at 00:38):

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

Bryan Gin-ge Chen (Jan 10 2021 at 00:39):

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

Mario Krenn (Jan 10 2021 at 00:45):

Thanks a lot, remarkable!

Kevin Buzzard (Jan 10 2021 at 01:23):

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 (Jan 10 2021 at 01:26):

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!)


Last updated: Dec 20 2023 at 11:08 UTC