Zulip Chat Archive

Stream: Lean for teaching

Topic: Running an intro to Lean workshop

Jake Levinson (Feb 25 2023 at 19:56):

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 (Feb 25 2023 at 19:59):

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 (Feb 25 2023 at 20:06):

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

Eric Wieser (Feb 25 2023 at 20:07):

But local installations are a good thing to encourage too

Jake Levinson (Feb 25 2023 at 20:08):

What is gitpod?

Kevin Buzzard (Feb 25 2023 at 20:09):

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 (Feb 25 2023 at 20:10):

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

Kevin Buzzard (Feb 25 2023 at 20:11):

Gitpod is the "online play" link mentioned here

Jake Levinson (Feb 25 2023 at 20:12):

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 (Feb 25 2023 at 20:12):

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

Kevin Buzzard (Feb 25 2023 at 20:12):

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

Last updated: Dec 20 2023 at 11:08 UTC