Zulip Chat Archive

Stream: Lean for teaching

Topic: Xena summer workshop 2022


Kevin Buzzard (Oct 03 2022 at 09:19):

Last week I ran a one-week summer workshop for undergraduates. I had £30000 + $10000 to pay for it and I suspect I spent all of it. I ran the whole thing myself pretty much (with 0 experience on the practicalities of workshop running). I'm just mentioning it in case anyone else wants to try this sort of thing. Here's how it worked.

The workshop ran for a week at the end of September. I advertised it in something like late June and the deadline was something like mid-July. The idea was that an undergraduate applied, and if they were accepted I would pay for their accommodation for a week in London and also any travel expenses for travel wholly within the UK. I thought that this would deter non-UK people from applying but it didn't; people came from the US, Korea, and several countries in mainland Europe. It would have been even more international were it not for the fact that I learned too late that if you start telling people from Turkey or Ukraine or Peru at the end of July that they've just won a trip to London in September, then 8 weeks is nowhere near long enough to sort out a visa. I was totally blindsided by this because I only expected people in the UK to apply.

So on 26th September around 30 undergraduates showed up at Imperial, and here's what we did. Every morning I would do two hours of live Lean coding doing just basic stuff related to mathematics in Lean (examples of structures, lattices, dot notation, finite sums, etc etc: most of the topics were suggested by the students). And every afternoon the students would work in groups of 4 on projects. I had eight project leaders (Bhavik, Yael, Maria Ines, Oliver Nash, Chris Birkbeck, Ashvni, Jason KY and Alena Gusakov, some of whom I also had to put up in London for a week but some of whom were here already) and I got each of them to put up a repo on github with some kind of a project in, and the idea was that the students worked on them, supervised by the leader. Then at 4pm we'd get together and one of my PhD students (Amelia, Jujian, David Ang) would give a talk to them about some more advanced stuff, and then that was it.

It was an in-person workshop and one of the things I'm getting from the feedback was that these people really enjoyed hanging out in person and getting to meet each other. I would clear off at 5pm and let them socialise amongst themselves. We didn't use Zulip for discussions, we used threads on the Xena Discord, which worked fine for these people.

My experience with things like this is that many students work on the project for a week and then just forget about it. But hopefully some of them will continue to experiment even though term is now starting across the UK.

Agnishom Chattopadhyay (Oct 05 2022 at 15:09):

This sounds great! Do you plan to share any of the material that was used in the workshop, like Lecture Notes or videos?

Agnishom Chattopadhyay (Oct 05 2022 at 15:12):

By the way, some people believe that Discord is not a great way to do certain things: https://alexn.org/blog/2022/04/09/scala-gitter-discord-mistake/

Although, this criticism may not apply to this situation

Kevin Buzzard (Oct 05 2022 at 20:48):

There are no lecture notes and no videos. Discord is perfect for a bunch of kids under the age of 21. Discord would be horrible for a forum such as this one.


Last updated: Dec 20 2023 at 11:08 UTC