Tuesday lectures

Stream: Copenhagen Masterclass 2023

[Kevin Buzzard]

During the social on Monday evening I asked a bunch of people what they wanted to hear from 9 to 10 on Tuesday, and my impression is that people want to see more live Lean coding. So my plan is to spend some time doing some basic stuff (e.g. talking about presheaves and sheaves and stuff, and doing basic exercises in Lean in preparation for Adam's talk), and also spending some time looking at some of the code which the audience wrote on Monday. Thank you all for being so engaged! People who are already Lean-competent and know the mathematics involved are welcome to skip my talk, but my impression is that there are plenty of people registered for the conference who know something about the maths but have very limited Lean experience, and I guess one goal we can have this week is to get these people to the point where they realise they can contribute to this project.

After me, Adam will speak about this fundamental fact that sheaves (of e.g. types) on ExtrDisc, Profinite, and CompHaus, are all "the same thing".