Workshops

Stream: Lean for the curious mathematician 2020

[John Mercer]

Hi all, i'm new here and interested in learning Lean. Is there any upcoming zoom workshops? Thx! John

[Alex J. Best]

Hi John, welcome! There are no upcoming workshops like lftcm2020 planned, but the videos from that event are all on youtube at https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N&index=1&ab_channel=leanprovercommunity. The first thing people did at that workshop was play through the natural number game http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/. And there are other resources to learn Lean at https://leanprover-community.github.io/learn.html

[Scott Morrison]

We had talked, during the wrap-up for LftCM2020, about organising a zoom "office hours" on some regular basis. I wonder if we might pick that idea up again.

[Kevin Buzzard]

On Friday 5pm UK I'm giving a talk about equivalence relations in lean on the Discord and then we're splitting into small groups and working on problems with a group of more experienced people helping out beginners

[Kevin Buzzard]

I will be assuming people have played through NNG and know what an equivalence relation is. It's really a workshop for undergraduate mathematicians

[John Mercer]

Oh that's awesome @Alex J. Best thanks so much for the YT videos!