Thursday teaching panel

Stream: Lean Together 2021

[Rob Lewis]

Tomorrow we have a session on "Teaching with Proof Assistants." This will be panel style. There are six presenters who will each give a short intro to how they've used proof assistants in the classroom/with undergrad students. Then we'll have an extended Q&A -- you can direct questions to individual panelists or to the group as a whole.

[Rob Lewis]

The idea here is, lots of people have expressed interest using proof assistants (Lean and others) in teaching (both math and CS). We wanted to show a range of what people have done, to give inspiration.

[Rob Lewis]

The panelists will be Jeremy Avigad, Jasmin Blanchette, Heather Macbeth, Gihan Marasingha, Patrick Massot, and Julien Narboux (order TBD soon).

[Rob Lewis]

Let's go in this order, based on my vague ideas about what each of you will say:
@Jasmin Blanchette @Jeremy Avigad @Julien Narboux @Heather Macbeth @Gihan Marasingha @Patrick Massot

[Gihan Marasingha]

I hope civilisation will still exist tomorrow.

[Rob Lewis]

Oh, also, panelists: if you're planning to share a screen, let's do a quick screen sharing test at the end of the coffee break before, to try to minimize transition time.

[Alexandre Rademaker]

Nice. Maybe we can list here the courses that people taught ?? My experience is with logics and discrete math

[Rob Lewis]

That's a good idea! Feel free to share the materials you've used too if you'd like.

[Rob Lewis]

A while back, Jeremy put together a nice list: https://avigad.github.io/formal_methods_in_education/

[Gihan Marasingha]

My principal shareable resource is a set of Lean problem sheets: https://github.com/gihanmarasingha/mth1001_tutorial. I've started writing notes based on these à la Mathematics in Lean https://github.com/gihanmarasingha/mth1001_sphinx. Very much in a draft state!

This was all for a first course in pure mathematics for a cohort of ~260 first-year UK mathematics undergraduates.

[Julien Narboux]

There are a lot of people teaching software foundations (semantics, hoare logic,) using Coq, Isabelle, ... there are also a lot of people using proof assistants for teaching logic (meta theory and or proof in natural deduction or variants). I am aware of very few experiments teaching with ITP a course with significant mathematical content. I know a few experiments about using ITP in an introduction to proof course. For example: https://math.unice.fr/~ah/div/bghp.pdf Hirschowitz Pottier experiment using CoqWeb (a proof by pointed web layer above Coq. I have a course about introduction to proof, and we are using Edukera. I will tell about that tomorrrow.

[Rob Lewis]

I think this was a fascinating discussion!

[Rob Lewis]

One thought I wanted to bring up: what kind of technology would help with these classes? I don't mean libraries, documentation, exercises, but more in the way of infrastructure. Better tools for installation were mentioned and that's definitely an important point.

[Adam Topaz]

I wonder if nix is a good approach with this? How hard is it to install nix (the package manager)? I've never tried installing the package manager itself (although I did use nixos for a little while)

[Patrick Massot]

Julien mentioned trying to get an open source version of Edukera where teachers can write exercises and choose the available lemmas and "tactics". And of course we all thought it should be based on Lean 4. That could be really nice but it's a huge engineering task.

[Heather Macbeth]

The Lean web editor was very useful for me, but it would be even more useful if it was 10x faster. Could that ever be improved?

[Patrick Massot]

Edukera has no performance issue that I remember of.

[Patrick Massot]

So there is hope to have enough of a proof assistant in the browser.

[Heather Macbeth]

I suppose CoCalc is also more efficient than the web editor. @Gihan Marasingha ?

[Patrick Massot]

CoCalc is no so much faster in my experience but it comes with a lot of goodies.

[Patrick Massot]

You can see what students are doing, chat with them, have video conferences, distribute stuff and get back assignments etc.

[Gihan Marasingha]

Agreed!

[Kyle Miller]

Patrick Massot said:

Julien mentioned trying to get an open source version of Edukera where teachers can write exercises and choose the available lemmas and "tactics". And of course we all thought it should be based on Lean 4. That could be really nice but it's a huge engineering task.

If I remember correctly, Racket has multiple languages, some reduced versions specifically for teaching -- it would be cool (while also being a significant engineering task) if there were some similar interface to have teaching versions of Lean.

[Alex J. Best]

@Edward Ayers already mentioned prototyping widgets in the web editor, but also getting them in cocalc would really help too! This might be easier in 4 if using lsp would require less coordination from the cocalc team.

[Heather Macbeth]

@Gihan Marasingha, I am amazed that you could make a 260-student course work. Even divided into 3 groups of 80 (?), it seems overwhelming. I have found that one-on-one troubleshooting is the best way to help students (and grown mathematicians!) learn Lean, but at your scale, you must have taken a completely different approach.

[Alex J. Best]

Heather Macbeth said:

I suppose CoCalc is also more efficient than the web editor. Gihan Marasingha ?

I guess the answer depends on the user's computer!

[Heather Macbeth]

Lots of careful planning? Pre-prepared demos? An army of teaching assistants?

[Heather Macbeth]

Anyway, it is inspiring!

[Gihan Marasingha]

@Heather Macbeth other than the Lean sessions + standard maths lectures, there are fortnightly (face-to-face where desired) tutorial sessions with ~10 students per group, staffed by an army of tutors! Still, the engagement this year in tutorials was relatively low. Possibly a consequence of the pandemic.

[Gihan Marasingha]

Further, there were optional 'proof skills' sessions run by senior undergraduates James Arthur and Omar Harhara.

[Jeremy Avigad]

So maybe the bottleneck at that scale is training the tutors.

[Sebastian Ullrich]

@Patrick Massot mentioned the issue of not being able to walk around and look over students' shoulders in a lab thanks to the pandemic. @Jakob von Raumer and I will teach a Lean (4, probably?) course next semester that traditionally worked on that principle (except for using Isabelle). Does anyone have experience or thoughts on using gather.town or a similar service for simulating this experience? We just gave it a quick try and it seems like it could work reasonably well. The major limitation is that only one nearby person seems to be able to share their screen at the same time.

[Jakob von Raumer]

The other limitation seems to be that there's no way to switch to using it in "zoom mode", i.e. talking and presenting to everyone in the room.

[Rob Lewis]

Jakob von Raumer said:

The other limitation seems to be that there's no way to switch to using it in "zoom mode", i.e. talking and presenting to everyone in the room.

There is. You can set up "podiums" that allow this

[Rob Lewis]

If you go into the classrooms in the workshop space, I think you can try it out

[Jakob von Raumer]

I saw the podiums in the item list, but it said "no interaction"?

[Lukas Stevens]

We are using LiveShare such that the students can work together in small groups. You can just open amount of groups windows of VSCode and supervise them with that. I also ask them to share their screen in the breakout room such that you can immediately see what is going on. Of course, this could also work great in gather.town.

[Rob Lewis]

I'm pretty sure I tried it in the demo room and it worked, but not completely certain

[Jakob von Raumer]

Rob Lewis said:

I'm pretty sure I tried it in the demo room and it worked, but not completely certain

There's an orange circle next to the podium that looks suspiciously like it should have _some_ function :) We'll try it

[Lukas Stevens]

You circumvent the problem somewhat with LiveShare since all students in a group are working on the same buffer within VSCode

[Lukas Stevens]

I should mention, however, that the extension is free but proprietary.

[Jakob von Raumer]

I think we'll have students working on their own file each with the choice of looking at each others solutions

[Jakob von Raumer]

Lukas Stevens said:

I should mention, however, that the extension is free but proprietary.

So is gather.town :shrug:

[Lukas Stevens]

True, but for video conferences there is a FLOSS alternative, namely BigBlueButton.

[Lukas Stevens]

We use that to host the tutorials and LiveShare to faciliate group work in breakout rooms

[Jakob von Raumer]

Is VSLiveShare easy to set up?

[Lukas Stevens]

I would say yes

[Gabriel Ebner]

Lukas Stevens said:

I should mention, however, that the extension is free but proprietary.

code-server is open source, but you need a publicly accessible web server for it: https://github.com/cdr/code-server

[Lukas Stevens]

After installation you can login directly with GitHub or if there are issues follow these steps: https://www21.in.tum.de/teaching/fpv/WS20/installation.html#connecting-with-peers

[Lukas Stevens]

Gabriel Ebner said:

Lukas Stevens said:

I should mention, however, that the extension is free but proprietary.

code-server is open source, but you need a publicly accessible web server for it: https://github.com/cdr/code-server

Hm, LiveShare works on a peer-to-peer basis

[Gabriel Ebner]

So --link works already? This still looked a bit WIP in the readme.

[Lukas Stevens]

Sorry, I don't know what you are referring to. In LiveShare one person acts as the host, which also means that all console commands are executed on that persons computer and the others connect to that host. Then, all participants can edit the buffer of the host (concurrently).

[Lukas Stevens]

Ah, I see it now in the README of code-server.

[Sebastian Ullrich]

Adam Topaz said:

I wonder if nix is a good approach with this? How hard is it to install nix (the package manager)? I've never tried installing the package manager itself (although I did use nixos for a little while)

Btw, my dream for this is that there is nothing to install at all. There should be a script you can curl | sh that downloads a statically linked Nix binary, puts it and its store in a dot directory, and opens a shell that removes all of that again on exit unless you call a command for activating a permanent installation. This should actually be almost in reach on Linux except for a bug on Nix master related to local (user-namespaced) stores. There is no such option on macOS, so that would be still one less platform.

[Sebastian Reichelt]

The teaching panel was very interesting.
I'm developing a web-based ITP GUI that is (among other things) aimed at teaching, so I'd like to get in touch with potential future users.
One specific question: What is the minimum amount of material that needs to be well-supported for it to be useful?
(A prototype is at https://slate-prover.org/. You can get an idea what proof input looks like by going to e.g. https://slate-prover.org/libraries/hlm/Essentials/Numbers/Natural/Divisors%20are%20less%20or%20equal, clicking "edit", and then clicking the + next to "no proof".)

[Jakob von Raumer]

What ITP is that built on right now?

[Sebastian Reichelt]

Right now it is a custom ITP running directly in the browser, as there is a lot of interaction between the GUI and the (not-small) kernel. But I'd like to rebuild the kernel at some point, and Lean 4 looks like a good foundation for that. Especially because the logic I've implemented turned out to map comparatively well to Lean 3 (e.g. sets are handled somewhat similarly).

[Kevin Buzzard]

For the course I'm teaching which starts in 2 weeks, I was planning on running the two hour sessions as follows: our university forces us to use MS Teams so I was going to be there for 10 minutes giving an overview, and then I was going to send everyone to the Xena Discord, where I think it will be possible to look over people's shoulders. You can do voice chats and share screen and I am cautiously optimistic (I've run Thursday evening problem sessions at the Xena meetings and they've worked OK in the past).

[Julien Narboux]

Yes building a new open source kind of Edukera is a significant engeering task, maybe something like two man year for people experienced with this kind of dev. Edukera does have performance issues when one try bug exercises. If I remember well, this is Coq running in abstract machine compile to javascript. This is one of the reasons why It should be rewritten from scratch. It is possible to run Lean in the Browser client side ?

[Bryan Gin-ge Chen]

#webeditor :smile:

[Bryan Gin-ge Chen]

It's not nearly as sophisticated as JSCoq though; all of the compiled olean files have to be downloaded up front.

[Julien Narboux]

For use in the classroom I think we need:

• no installation and running client side in the browser, otherwise it won't scale to thousand of students
• integration with other educational systems such as moodle, for automatic grading (Edukera has this feature, it is really important when I have 400 students).
• nice notations (2D notations for Sigma, etc...)
• tutorial
• not two much things to type and not two much syntax to learn:
  In an Isar like language, one need to type the statements, but could prove each step by automation without learning the syntax of the tactics.
  In a Tactic style language, one need to learn the tactics.
  That is why I like the approach of Edukera which is a compromise between the two.
  As said during the talk, Edukera also has limitations: not open source and one can not create her own exercises.

Note, that I think the exercises for beginners learning proof should be mostly "deductive island" : proving something given some known lemmas, with enough lemmas allowing different solutions. For example, in geometry, the student should be able to use synthetic approach, or coordinate based approach.

Developing a whole theory, introducing relevant lemmas etc... is not for beginners, and I think it is rarely done in maths classroom.

[Patrick Massot]

I agree with all Julien just wrote and add that in my course students are never asked to write a definition or lemma statement. They do have to write some intermediate statements in proofs but they are very easy.

[EricGT]

Going a bit out a limb here.

One group I interact with that is involved in teaching computer programming and had many similar problems that evolved into a well liked and used group are teachers in the U.S.A. that teach the Java Advanced Placement course in high school. They use Runteone and for Java use Introduction to Programming with Java as the book but the group is well organized with a website (CSAwesome) and a private Google Group (Teaching CSAwesome) that you can ask to join but have to convince them you are a teacher as you then get access to the answer guides and such; usually an e-mail account of *.edu or such works.

I am noting this because getting everyone on the same page for how to setup a computer, what to teach, what works, what does not work, etc. seems to me to be the same set of topics but just replacing Java for ITP.

:smile: