One day tutorial

Stream: Lean for teaching

[Rémy Degenne]

With @Lorenzo Luccioli , we will give a tutorial about Lean/Mathlib to the members of our research team at the end of September. The tutorial will last one afternoon only (there will be a presentation about Lean in the morning). I would like to know if some people have experience running a short tutorial like this, as opposed to the week-long tutorials of workshops like LftCM. Any advice is appreciated, and I would be happy to know what you used as tutorial material and how it went.

The public will be roughly 15 machine learning researchers (PhDs and Postdocs mostly), who have never used a proof assistant. I plan to ask them to follow the installation instructions in advance as much as possible, to be able to use the few hours I have for something else, even though I fully expect the first hour to be dedicated to fixing installation issues.

I would like to try and make the tutorial about math that is a bit more interesting to them than simple manipulations of natural numbers or basic logic. I really want to convey the idea that they could be doing "real math" in Lean and not just toy problems, and I want to emphasize the use of tactics. At the same time, I fear that jumping into something more complex without mastering the basics of proofs in Lean first might be hard.

Did anyone organize such a short tutorial session? What did you do and how did it go?

[Johan Commelin]

2 years ago I gave a 1-day workshop at a Dutch math school. The audience consisted of maths PhD students (and some interested postdocs/staff). We mostly did NNG + a bit of MiL.

[Patrick Massot]

The repository https://github.com/PatrickMassot/GlimpseOfLean was created for such occasions. I used it a couple of times, and @Floris van Doorn also did.

[Rémy Degenne]

Thanks! I was thinking about extracting a few things from MiL, but it really is made for a longer learning experience so that looked difficult. And in particular I want to avoid ever saying the word "filter" in the tutorial :) .
That GlimpseOfLean repository looks like a very good fit for what I want to do!

[Patrick Massot]

We need to work more on such resources, because this is a fairly common task. I think Floris probably has useful things to say.

[Kevin Buzzard]

If you're worried about installation, let them use the live lean web thingy and just give them one file to work on

[Patrick Massot]

Nowadays using GitPod or GitHub codespaces is almost mandatory for a one day event.

[Miguel Marco]

Another option is to setup a local server with code-server and the Lean extension installed.

[Floris van Doorn]

Patrick Massot said:

The repository https://github.com/PatrickMassot/GlimpseOfLean was created for such occasions. I used it a couple of times, and Floris van Doorn also did.

A bit late to the party, but I have very good experiences with the Glimpse of Lean repository. I've used it for a 3-hour tutorial at the logic colloquium in Milan last year, and it was received very well. 3 hours is actually not quite enough to get to it, and I don't think anyone got to the "topics" part of the exercises, so this repo could also easily be used for tutorials that take longer, up to ~1 day. The fact that the topics folder is now logic-heavy is a consequence of me giving this tutorial at the logic colloquium.
Github codespaces and Gitpod work well for a tutorial like this, for the participants that are unable/unwilling to install Lean.

[Floris van Doorn]

Also, the first few exercises in Glimpse of Lean teach ring before rw and teaches the student to use ring for "trivial" stuff (commutativity, associativity) and rw for the rest. I think this is good for didactic reasons.

[Michael Rothgang]

In May, I (co-)organised a one-day Lean workshop. We were inspired by the LftCM schedule, and tried to present Lean first, but have exercises focused on practicing the basics. Presumably a glimpse of Lean is better developed, but I'll also drop the link in case it helps: https://www2.mathematik.hu-berlin.de/~rothganm/BerLean.html

[Rémy Degenne]

Thanks everyone for the feedback. We'll probably use Glimpse of Lean, in which we will add a new "topics" file related to probability (unless we discover during the preparation that doing simple probability with mathlib is still too unwieldy). I'll make sure to check that codespaces or gitpod works, but I'll try to get the more motivated participants to install it locally.

[Floris van Doorn]

Nice! Please make a PR to upstream the probability file afterwards.
It might be challenging to jump from logical connectives to probability theory, hopefully you can (mostly) avoid things like coercions.

[Rémy Degenne]

Your remark about coercions makes me think that I definitly don't want them to encounter the issue of dealing with ENNReal vs Real.

[Rémy Degenne]

On Friday Lorenzo and I gave the tutorial, using GlimpseOfLean. Here are some of my thoughts about it.

Around 10 people attended the tutorial (some of the PhD students, postdocs and researchers from our team). Some had to go early but 8 stayed until the end. That end happened after 3 hours and 15 minutes, when several attendees reached the end of the files they were working on around the same time and everybody decided they had enough. The reactions were positive and many of them enjoyed the game aspect of proving in Lean. GlimpseOfLean does a great job of introducing tactics one by one and the exercises are at the right difficulty. Two participants reached the end of exercise file 4, three got to the end of file 2, and the others somewhere in between. Nobody tried any of the topics files in GlimpseOfLean. We had prepared a file about probability (PRed to GlimpseOfLean by Lorenzo) but nobody got there.

About the setup: everybody except one attendee used gitpod. I was showing them on a screen as I was opening it and guided them step by step ("here you get red error bars, now click on 'restart file'", etc.). That worked well. The one who did not use gitpod did a local install on arch linux and emacs. The first install did not work and I don't really know why (and could not help) but he fixed it and customized his emacs for Lean as he was progressing through the tutorial. He did not find how to get information about how you type specific symbols (in vscode you hover over the symbol to see how to type it).

After that we proceeded with the GlimpseOfLean exercise files, and that mostly went smoothly. From time to time I would talk briefly about some other things about Lean. My goal was to give brief examples of what people were using Lean for. I showed the PFR project website and talked for two minutes about the collaborative aspect, then 30 minutes later I took two minutes to show an example of a Lean proof from Lorenzo's recent work about information theory; I also showed the mathlib doc; another time I talked for two minutes about loogle/moogle/leansearch.

Here are some common confusions from the participants, or questions they had:

• Lean is sensitive to indentation. Putting a space at the wrong place can give weird errors
• Is ring really a proof of something? ring is the first tactic introduced, and I think this is a great choice: they got confused for a bit but then they all saw the potential of tactics, which was great.
• If you have h : a = b and h' : b = c + d, why can't you write rw [h + h'] to rewrite with a + b = b + (c + d)?
• Some were confused for a while about the various things shown in the infoview and had trouble knowing where they were in the proof and what exactly was the goal. the fact that you can't see your goal clearly if you have an error did not help. This was particularly an issue with proofs of calc steps.
• When they had to show a = b using a calc proof, many wrote calc b = ... = a (starting with b) because that was the most convenient proof path, and then got surprised that their proof of b=a did not prove a=b. I introduced the symm tactic at that point (which is not among the tactics introduced in GlimpseOfLean).
• You can't deal with subtraction as if it was addition of the negative without rewriting it that way first. 0 + x needs an explicit step to be transformed into x. They expected a bit more automation at various such points.
  @Lorenzo Luccioli perhaps you recall other common questions?

Overall I think the tutorial went very well and they now all have a good idea of what Lean is about. I don't know if any of them will go further with it. At least two did part of the natural number game, so there is some interest.

[Lorenzo Luccioli]

A few other observations from my point of view:

• An attendee had some troubles with GitPod, I think the problem was with the two factor authentication that GitHub requires to log in from a new device. I guess this is not so common, but maybe it can be reminded before the tutorial that, if one is planning to use the remote options, a working GitHub account is needed.
• I tried to open the repo with Github Codespaces, it seemed to work but I think everybody used GitPod in the end.
• Someone tried to combine hypotheses using operations: from (ha : 0 < a) (hb : 0 < b) write ha + hb in order to have 0 < a + b.
• The fact that Lean encourages to use backward reasoning for proofs was challenging at first.
• I saw a bit of confusion when dealing with propositions, like in this example: (p q r : Prop) : (p → q) → (p → q → r) → p → r. I think the confusion was mostly linked to two things:
  • How to compose hypotheses dealing with abstract propositions? Maybe the most effective way in this case is to highlight the fact that an implication can be treated just as a function. I also found helpful encouraging the use of have := h1 h2 to see in which way things can be composed and be able to use forward reasoning.
  • The fact that the parentheses are only explicit when we want to associate on the left. How do I know what intro does in the above example?

[Patrick Massot]

Thanks, this is all useful feedback. Don’t hesitate to open PRs if you have suggestions for improvements.