My current plan for the first few weeks is to write a blog post for each one the items that I’ve listed in my projects. For no better reason other than this is the first one listed on the page, I’ve decided to talk about my experience organizing and running the “Learning Lean Seminar”. First I should mention that all of the content from the seminar can be found here.
The intended audience for the seminar are undergraduate Math and CS students at Northeastern University where I’m currently in my last semester of my postdoc. The original goal was to get a group of undergraduate students introduced to Lean with the express purpose of using it as an interactive theorem prover, and contributing to mathlib. This goal meant I haven’t spent much time talking about applications of formal verification outside of formalizing proofs in math. I also didn’t want to introduce too much abstract theory, so I only touched on the topic to the extent of mentioning things like the Curry-Howard correspondence.
The actual attendance has turned out to be more CS-focused, with some graduate students also getting involved. Given the attendance I’ve mentioned some more aspects of formal methods in general, but the focus has still largely remained on formalizing proofs for mathlib. The sessions are mostly structured as coding demos where I work through a few extended examples in a Lean document. The sessions have decent live attendance with many questions, but I also record the lectures through Zoom for people who cannot tune in in person. I also aim to assign some “homework” every week. For the homework I’ve found it very helpful not to reinvent the wheel, but use some of the great Lean learning tools and resources. In the github page all the relevant links are included, but the two highlights for the students so far have been the Natural Number Game and Lean for the Curious Mathematician 2020.
So far the focus has been less on the explicit tactics used in proofs, as I defer that to the learning resources. I find that learning those kinds of mechanics requires much more time and repetition that I can provide once every week. The NNG and some of the LFTCM2020 exercises are excellent learning tools for exactly this kind of scenario. Instead I have been picking up with exactly how the math is formalized in mathlib, and how to reason about it. In particular, I’ve focused on how to prove things about and construct things out of structures and classes. I started small by proving things about enumerated inductive data types, moving to simple structures like pointed types, and finally doing a kind of “accelerated” version of the NNG with semigroups.
A stretch goal for the semester was always to have a group of students that were prepared to begin contributing to mathlib. The end of the semester is quickly approaching, and it seems like I may be missing that goal by a few weeks. My hope is that I can remain in contact with the students and continue with so, and hopefully by the summer we can submit a PR to mathlib with a new piece of formalized mathematics.
My original motivation for running this seminar was that I wanted a better working knowledge of Lean to further my own goals of formalizing aspects of commutative algebra for mathlib. The best way I can learn a subject is to force myself to teach it to other people, either in the form of a learning seminar talk, or learning real analysis for the first time when I had to teach the course to undergrads. I’ve found the experience has helped a ton towards achieving my goals, and so for a kind of selfish reason I would consider the experiment a success. Though we are far from the end of the semester, so I may have to revisit this at the end of the semester.