Feedback from my seminar

Stream: Lean for teaching

[Michael Stoll]

In the last winter semester, I ran a "seminar" on "Formalizing results from number theory". (I put "seminar" in quotes, since I declared it as a seminar, because no other available category fit better, but it was more like project work.) The idea was that students would form small teams and each team would try to formalize some result from Chapter 17 (on Diophantine Equations) in Ireland-Rosen. We had an online meeting every Wednesday morning, where the students could ask questions or describe problems they encountered, and I would try to answer or solve them. In the first week I gave a live demonstration (putting together a proof of the easy direction of the three-squares theorem).

There were five participants (plus two more students joining in on Wednesdays; one is writing her bachelor's thesis, the other one her master's thesis on some formalization project, so they could discuss their questions as well), who split into three teams (2+2+1). One team did Sophie Germain's theorem, one did the proof that of x^3 + y^3 = a has one rational solution for an integer a > 2, then ir has infinitely many, and the team of one did Pell's equation. (All in lean3 + mathlib.)

• All three projects were successful: by the end of the semester, they had a somplete (sorry-free) formalization.
• The resulting code tended to be rather long-winded. A second iteration with some hints as to how one can write certain things more (space-)efficiently (e.g., avoid repetition by pulling out re-usable statements as separate lemmas) led to significantly shorter code (but still quite far away from, say, mathlib standards).
• Feedback from the students:
  • The live demonstration in the first session was quite helpful
  • The Natural Number Game (which I receommended they try first) was very helpful
  • They tended to have difficulties with coercions (nat <--> int, mostly, due to the topic)
  • Finding the relevant lemmas in the library was also frequently a problem
  • The online sessions did help them a lot with getting unstuck when they had problems

On the whole, it was a quite positive experience (I had no idea how it would go when I started it). When I do something similar next time, I will add some lecture or similar on how to write reasonably efficient code, in the hope that the code that gets written is less bloated from the beginning.

[Kevin Buzzard]

Something which my students seem to like (and my understanding is that you didn't do this) is a lot of me live coding, working through examples of relevant mathematics in lean. But clearly it seems that you have got a winning formula here. For me, getting the students writing code which compiles is the big win. Mathlib is a much harder mountain to climb and I'm more and more wondering whether for some projects it's best to just stick them up on GitHub and write a good readme. Of course if the students are prepared to put in that extra work then they will learn more, but my experience, sadly, is that a lot of people in courses will show up, learn the system, write compiling code and then disappear. So one has to decide what the goals are here, and my goals recently have been to just get more mathematicians doing lean rather than making mathlib.

[Kevin Buzzard]

PS congratulations on successfully running the course! It takes a certain amount of guts to be the person at the front claiming that you'll be able to solve everyone's problems in real time.

[Michael Stoll]

I'm glad I was able to solve their problems, mostly in real time (sometimes I had to go on a reasearch expedition in mathlib after the meeting, though...).

[Michael Stoll]

But it was a lot of fun; you never know what to expect.

[Michael Stoll]

I actually did quite some bit of live-coding in the meetings (of lemmas that might be useful), depending on the questions that were asked.

[Michael Stoll]

The goal was never to produce something for mathlib; I don't think that is reasonable in such a setting.
I'm using the Pell equations code produced by one of the students as a basis of what I am doing to get the results into mathlib, but it is still quite some work getting it into acceptable shape for that purpose.
The other two results are, I think, too specialized anyway to be a reasonable mathlib addition.

[Kevin Buzzard]

If you are still able to get the students to spend time on their projects then just encourage them to make some standalone thing on GitHub with an explanation of what they did. The difficulty at the end of a course is that then students have to start worrying about other courses and if they didn't get totally addicted to lean (and the majority don't, they wanted to find out what it was about and now they know and so their aim is achieved) then you might never hear from them again, so now's the time to get them to get it up online in a presentable form