Course in Edinburgh 2023

Stream: Lean for teaching

[Patrick Kinnear]

Hi everyone!

I am new here. David Jordan and I are based in the School of Maths at UoE, and are planning to run a pilot course this semester on Lean aimed at graduate students in algebra, topology, geometry, category theory etc. This is part of the group's aim of delivering some form of programming relevant to grad students in algebra and related fields. We though Lean might be more interesting than just going over a computer algebra system, and it might be more of a level starting point since Lean could be quite different to the sorts of languages the students are most likely to have met before.

David and I are just starting out learning Lean ourselves, so the course will be very studentled and collaborative. A reasonable goal for the course would be that participants learn how to interact with the Lean environment, and to access the existing library of mathematics, and that by the end we are able to venture into proving new theorems (i.e. translating known theorems from our discipline) into the library. So we will probably start with some tutorials and then move more towards some project-based work.

We are still at the stage of planning how exactly the course will run. I wondered if anyone has been in a similar position to us (learning Lean by teaching a grad course) and has any wisdom to share?

Let me know if you have any thoughts, suggestions for teaching, project ideas, or any other interest in this pilot course.

Thanks,

Patrick

[Kevin Buzzard]

I gave a Lean graduate course in 2021 targetting mathematicians; it comprised of 8 two-hour workshops all run online (on Discord) because of the pandemic. Here's the repo https://github.com/ImperialCollegeLondon/formalising-mathematics .

[Patrick Kinnear]

Kevin Buzzard said:

I gave a Lean graduate course in 2021 targetting mathematicians; it comprised of 8 two-hour workshops all run online (on Discord) because of the pandemic. Here's the repo https://github.com/ImperialCollegeLondon/formalising-mathematics .

Thanks, I didn't know about this, looks like a great resource!

[Jeremy Avigad]

I just mentioned the course I taught at Carnegie Mellon in the general stream. Also: have you been in touch with Tobias Grosser and his team at Edinburgh, or Paul Jackson and his student, Ramon Fernández Mir? they all have experience with Lean.