Formalising Mathematics 2022 Imperial course

Stream: Lean for teaching

[Kevin Buzzard]

So I taught a course last term. it was for 3th and 4th year students doing Bachelors and Masters degrees. Here's some details.

The material: there's a Github repo, there are online course notes and a Formalising Mathematics 2022 Youtube playlist.

The course notes were a big experiment. @Edward Ayers convinced me that should I stop producing pdf course notes and that I should focus on a web based solution. I tried Sphinx and you can see the results on the course notes link above. A lot of the students said that Part B was the most helpful.

The Lean repo: I made the decision to never upgrade mathlib; so you use the command line once during installation and then after that you click pull in VS Code and it just works. This caused problems, but they were my problems, not the students' problems.

The course was assessed by 3 projects; each involved writing about 200-400 lines of code (including comments) and a 5-7 page pdf file (numbers went up as the projects got more ambitious; the projects were worth 20%, 30% and 50% of the grade, and I was very pleased with this because clearly the ability of the students went up during the course; at the end they could all write competent Lean code). The subject of the projects: "something I learnt in year 1", something I learnt in year 2", "something I learnt this year". I was extremely flexible, eg Jason KY asked if he could just submit a measure theory PR for his first project and I said "sure" even though he didn't learn it in year 1.

The material I covered: this was a bit of a shock. I'd given a graduate course before and had intended to recycle the material, but because of the nature of the assessments the students did not want to hear about filters/uniform spaces (they didn't see them in other courses!); they wanted to see number theory, graph theory etc because these are the courses they're doing right now. This caused rather a lot of last-minute reorganisation.

Here's an overview of some of the final projects.

There were a fair few in number theory. Examples: If 2^n-1 is a Mersenne prime then 2^n-1(2^(n-1)) is a perfect number, Existence of a nontrivial solution to Pell's equation, Hensel's lemma for complete normed fields. I'm not sure if any of these are in mathlib but in general the code the students were writing is not mathlib-ready. I've never really worried about this -- my goal has always been getting the students to do maths in Lean, not to write mathlib. Someone tried Lagrange's four squares theorem but didn't finish (this didn't bother me either -- sorrys were fine). Someone got most of the way to a classification of all integer solutions to x^2+1=y^3 .

Someone proved a theorem about nonempty convex subsets of Hilbert spaces (distance to a point attains a minimum on such a set). Someone proved CRT for two coprime ideals of a commutative ring.

There were several category theory projects (Ken Lee and Joseph Hua, who wrote the HoTT game, both came to the class, and their influence rubbed off a bit). Someone (using quite recent work of Yael I think) proved an adjunction between topological spaces and frames. Someone proved an equivalence of two categories associated to a presheaf P; the category of presheaves over the category of elements of P is equivalent to the overcategory of P. Someone got 95% of the way towards defining the boundary map in the snake lemma for an arbitrary abelian category.

There were a couple of graph theory projects -- one on Eulerian graphs and one on products of graphs. Graph theory is a popular 3rd year course here.

Someone proved one direction of something they called the fundamental theorem of asset pricing, someone did something involving completeness of lambda-calculus. These people could do this because my rules this term were very flexible, but I found these projects hard to mark; next year I think I will demand that the projects are on topics covered by pure maths courses. That might push attendance down but this year was the first year the course ran so people were scared by it; next year I suspect attendance will go up anyway.

Some people insisted on defining things we have already, e.g. Euclidean domain (perhaps because the version in mathlib "isn't the same as the version in my notes"). This was fine as far as I was concerned.

I asked students to submit a Lean file, a toml file and a pdf file. Some students for their project just submitted a Lean file and a pdf, and I just used the toml file from the course repo because these students don't know how to make another repo, they just click VS Code and they make a new Lean file and write import tactic at the top and it just works.

The main problem I had was with students saying "well you could do 2 hours on uniform spaces but how would this help us? Why not do 2 hours on graph theory instead?" which meant I had to learn the graph theory API :-) This was the main problem I had with not upgrading mathlib -- Kyle was in the process of writing a bunch more graph theory API in Jan-Feb and we didn't have access to it in the course repo. However the students doing graph theory were sufficiently savvy to know how to bump mathlib locally, and at some point I just cut and pasted some graph theory API from March mathlib into a new file in the repo and imported that instead.

The course notes: I still have not quite worked out how to teach. I think that sets and functions need to be a bit earlier, and I think that to teach structures I should just import data.real.basic and then roll my own complex numbers. I did not do this this year; I don't quite know whether I should now edit the course notes (the course is over and the projects are all handed in and marked so I can do what I like with the notes really, but if I start changing the notes now then they won't match up with the videos).

I will be teaching the course again in Jan 2023 and by then I suspect that it might be viable to do it in Lean 4, so I'll have to rewrite everything anyway.

[Johan Commelin]

Thanks for this write up! I look forward to teaching a course about/with Lean. And all your experiments will be very valuable info.

I don't quite know whether I should now edit the course notes (the course is over and the projects are all handed in and marked so I can do what I like with the notes really, but if I start changing the notes now then they won't match up with the videos).

I will be teaching the course again in Jan 2023 and by then I suspect that it might be viable to do it in Lean 4, so I'll have to rewrite everything anyway.

I would just freeze the repo, and make edits in the 2023 edition of the repo. Causes the least confusion to random visitors.

[Filippo A. E. Nuccio]

Thanks for the story and the feedback, very enlightening. One question: would it be possible to run the exercices on the web editor, if I wanted to cherry-pick some of them for a crash course I will be teaching in May to people who might not have Lean installed locally?

[Kevin Buzzard]

I conjecture that everything will work fine on the web editor. The reason I didn't use the web editor at all was simply that I knew I was forcing the students to write Lean code and so I thought we'd go through the pain of installing early on because it would save them from getting addicted to the web editor.

[Filippo A. E. Nuccio]

Great, I see. And do you know how to prepare html links to the web editor with the chosen exercices? Like the ones in the Lean Community Website?

[Kevin Buzzard]

Yes. First find the page you want to interact with on GitHub in the repo. Then click on "raw". Then cut and paste the URL into the relevant box in the lean web editor. The resulting URL is the one which you can pass onto others.

[Filippo A. E. Nuccio]

Thanks!

[Bryan Gin-ge Chen]

Filippo A. E. Nuccio said:

Thanks!

One warning is that the web editor gets updated nightly to the latest version of Lean 3 + mathlib, so such links might not be very stable.

[Filippo A. E. Nuccio]

Ah, so there is no way to run online files using old versions of mathlib?

[Bryan Gin-ge Chen]

Unfortunately not. It could probably be done, but it'd be a lot of work and I've been hoping that Lean 4 will somehow magically make this all irrelevant.

[Filippo A. E. Nuccio]

I see, no problem! Thank you, at any rate, I will probably play with very basic structure that won't run the risk of changing overnight.

[Kevin Buzzard]

Another possibility is that you just host your own lean web editor, this is certainly possible (e.g. I host NNG which is lean web editor + more)

[Kevin Buzzard]

then for your version you can just leave mathlib at a fixed version

[Kevin Buzzard]

like NNG stays on Lean 3.4.2.

[Filippo A. E. Nuccio]

Ah, good. And is it hard to host my own lean web editor? Do you do on your personal git or on the server at Imperial, or something else?

[Kevin Buzzard]

You'll have to ask someone like Patrick or Bryan how to do it; I use lean-game-maker to make NNG but you won't need that, you will just need pretty much the same code as is making the web editor. Yes I host it on Imperial's servers which have been really flakey recently.

[Filippo A. E. Nuccio]

OK, thanks. I will think about the best solution (I think that at the end of the day I can make do by having mathlib updated as long as I plan to make students play with basic set theory and topology, that won't probably evolve).

[Bryan Gin-ge Chen]

Oh yeah, it's not too hard to host your own web editor (hopefully). If you follow the instructions here you can copy the resulting dist folder into a different repo and use GitHub pages to publish those files to the web.

[Filippo A. E. Nuccio]

Oh, very nice. I might come back with some questions when I start preparing my classes, but if I undestand correctly you are saying that as long as I can create this dist folder somewhere (eg. on my laptop) then I can include it in some git repo and make it public, without asking the IT people in my department?

[Bryan Gin-ge Chen]

Yep, pretty much!

[Kevin Buzzard]

yeah, for example you could host it all on github pages

[Jukka Kohonen]

Nice course, this is. Do you have any preference how people should submit corrections to the problem sheets, if they have any? (I have a trivial correction to section14polynomials/sheet01degree.lean: in the comments surely you want deg(f*g)=deg(f)+deg(g), not *.)

[Kevin Buzzard]

Oh thanks! I fixed it :-)