New year, new teaching material

Imperial College has gone back to in-person teaching so I have 250 new subjects to experiment on, namely the new 1st year maths undergraduates.

I’ve spent a few years now trying to figure out how best to teach maths undergraduates how to get up to speed quickly with Lean, a theorem prover which uses dependent type theory and has a large mathematics library. In theory students can do all of the problem sheets I give to them in Lean. In practice things aren’t nearly so simple. As well as a long list of tactics to internalise, it helps if students get a feeling for what’s in Lean’s maths library already, and perhaps they should also know the difference between definitional and non-definitional (i.e. propositional) equality. Unfortunately definitional equality is a non-mathematical concept, in the following sense: if you define addition on the naturals recursively by n+0:=n and n+(succ m):=succ (n+m) then n+0=n is true by definition and 0+n=n is not. This is an asymmetry which is of no relevance in real-world mathematics.

This year I’m still avoiding talking about definitional equality, and I’m also avoiding talking about the example sheet questions which I’m giving to my class. A typical example sheet question, even if easy from a mathematical point of view, may only yield to someone who is armed with a whole bunch of Lean tactics. So this year, instead of encouraging the students to work on the example sheets, I’m encouraging them to work on easier problems, so that we can build up to the example sheets later.

The 2021 Lean course home page is here, and I’m making an associated collection of short videos here . I’m going through basic tactics one by one, making what I hope is a more comprehensible introduction to doing mathematics in Lean. All the Lean problem sheets I’ve written so far can be tried online without having to install Lean, but installation instructions for those who want a slicker experience are here. 1st years are busy with their coursework right now, but when it’s over hopefully I will be able to get some feedback from them and others about this new approach. At the time of writing, I have finished the logic sheets, and I’ve just started pushing sets sheets. Still to come: functions and binary relations.

Next term things are getting much more serious. I’m actually teaching an official Lean course as part of our undergraduate program. In contrast to what I’m doing this term (evangelising), next term (Jan to March 2022) I will actually be figuring out how to get students to engage with some more serious undergraduate mathematics. Students will be examined by a series of projects, in contrast to the usual approach here for final year courses (a closed book exam under timed conditions). I’m going to cover standard topics like basic analysis and topology, and also more esoteric ideas like filters and perhaps uniform spaces. Should be interesting! This will involve yet another repository, which I suspect will be to a certain extent based on this one. But more on that later.

Advertisement