LFTCM2020 port

Stream: maths

[Kevin Buzzard]

Are there any plans to port the LFTCM2020 exercises to Lean 4?

Yesterday I ported the category theory exercises and half of the solutions, and uploaded them to the Copenhagen Masterclass repo because the masterclass will be quite category-theory heavy and I thought that the exercises might be good practice for the students. But I don't want to be causing confusion if there are plans to port this stuff elsewhere (or indeed if it's already been ported!)

[Patrick Massot]

I think only the differential geometry and category theory exercises are not yet superseded by MIL and hopefully we will eventually have also chapters about those advanced topics (at least at the level of very superficial introductions as in LFTCM2020).

[Kevin Buzzard]

Yes it did occur to me that the material most of the exercises were now covered more comprehensively elsewhere; I was motivated to translate the category theory exercises precisely because as far as I knew they were not.