Running an intro to Lean workshop

Stream: Lean for teaching

[Jake Levinson]

Hi all, I'm hoping to run an introduction to Lean workshop at my institution in early May. This will be a single 2-hour session, so I'm hoping to structure it as partly hands-on and partly a demo. I may be able to ask attendees to install Lean in advance, but I'm not certain of it.

1) Would you recommend just having attendees use the Lean web interface? Alternately, should I hold a pre-workshop "help with installing Lean" session?

2) Has anyone done a single-session workshop like this before? If so, any suggestions would be totally welcome.

I'm thinking of something like the following:

• (10 minutes) Briefly show the Natural Number Game so attendees can find it later if they're interested and don't have Lean installed
• (30 minutes) Demonstrate a couple of proofs in Lean -- first something elementary to demonstrate tactics, then something more high-level to demonstrate how one builds up lemmas and an API.
• (60-80 minutes) Attendees work on a structured set of problems, e.g. part of an LftCM workshop problem set.

My goal is to get attendees equipped to continue working on Lean after the session -- so the installation and other technical hurdles will be taken care of, and they've done some 'basic' proofs on their own. That seems like the best way for attendees to come away with something real.

[Kevin Buzzard]

I would tell everyone to install beforehand and only let on on the day that if you failed then there's another option ;-)

[Eric Wieser]

Using gitpod is usually a more pleasant experience than the (lean3) web editor: it has widgets and performs better.

[Eric Wieser]

But local installations are a good thing to encourage too

[Jake Levinson]

What is gitpod?

[Kevin Buzzard]

The main problem I suspect you'll have with your setup is that it takes a lot of time to learn the standard finite list of tactics and lemmas necessary to work on problems in a given area. With NNG you can get all the way to (x+y)^2=x^2+2xy+y^2 with three tactics and building your own lemmas. The moment you branch out to more serious mathematics you need to know about ten basic tactics and also perhaps a bunch of standard lemmas depending on what you're doing. If you look at my course this year I think I've managed to find a way through which minimises the pain, but there's a lot of basic logic involved to get students proficient with about ten tactics before we start on real numbers and limits.

[Jake Levinson]

Oh I see. Do you recommend people do the NNG before attempting actual Lean?

[Kevin Buzzard]

Gitpod is the "online play" link mentioned here

[Jake Levinson]

I still think it would be good to show a demo of serious mathematics, just to show people what to be working towards. That it's not all elementary logical manipulations, and that eventually you (hopefully) get to write proofs that sound a bit closer to human-level reasoning, with elementary details taken care of.

[Jake Levinson]

(But this wouldn't be part of the hands-on stuff)

[Kevin Buzzard]

As you can see I get into limits of sequences asap but before that I do a bunch of logic. Patrick's tutorial also goes straight for real analysis; this is also definitely worth looking at