Zulip Chat Archive

Stream: Lean Together 2021

Topic: Thursday teaching panel


view this post on Zulip Rob Lewis (Jan 06 2021 at 09:43):

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.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:44):

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.

view this post on Zulip Rob Lewis (Jan 06 2021 at 09:45):

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

view this post on Zulip Rob Lewis (Jan 06 2021 at 20:11):

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

view this post on Zulip Gihan Marasingha (Jan 06 2021 at 20:14):

I hope civilisation will still exist tomorrow.

view this post on Zulip Rob Lewis (Jan 06 2021 at 20:29):

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.

view this post on Zulip Alexandre Rademaker (Jan 06 2021 at 20:31):

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

view this post on Zulip Rob Lewis (Jan 06 2021 at 20:32):

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

view this post on Zulip Rob Lewis (Jan 06 2021 at 20:32):

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

view this post on Zulip Gihan Marasingha (Jan 06 2021 at 20:42):

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.

view this post on Zulip Julien Narboux (Jan 06 2021 at 20:45):

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.

view this post on Zulip Rob Lewis (Jan 07 2021 at 17:02):

I think this was a fascinating discussion!

view this post on Zulip Rob Lewis (Jan 07 2021 at 17:04):

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.

view this post on Zulip Adam Topaz (Jan 07 2021 at 17:05):

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)

view this post on Zulip Patrick Massot (Jan 07 2021 at 17:11):

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.

view this post on Zulip Heather Macbeth (Jan 07 2021 at 17:12):

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?

view this post on Zulip Patrick Massot (Jan 07 2021 at 17:13):

Edukera has no performance issue that I remember of.

view this post on Zulip Patrick Massot (Jan 07 2021 at 17:13):

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

view this post on Zulip Heather Macbeth (Jan 07 2021 at 17:13):

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

view this post on Zulip Patrick Massot (Jan 07 2021 at 17:14):

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

view this post on Zulip Patrick Massot (Jan 07 2021 at 17:14):

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

view this post on Zulip Gihan Marasingha (Jan 07 2021 at 17:15):

Agreed!

view this post on Zulip Kyle Miller (Jan 07 2021 at 17:15):

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.

view this post on Zulip Alex J. Best (Jan 07 2021 at 17:17):

@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.

view this post on Zulip Heather Macbeth (Jan 07 2021 at 17:19):

@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.

view this post on Zulip Alex J. Best (Jan 07 2021 at 17:19):

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!

view this post on Zulip Heather Macbeth (Jan 07 2021 at 17:19):

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

view this post on Zulip Heather Macbeth (Jan 07 2021 at 17:20):

Anyway, it is inspiring!

view this post on Zulip Gihan Marasingha (Jan 07 2021 at 17:46):

@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.

view this post on Zulip Gihan Marasingha (Jan 07 2021 at 17:48):

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

view this post on Zulip Jeremy Avigad (Jan 07 2021 at 17:56):

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

view this post on Zulip Sebastian Ullrich (Jan 07 2021 at 17:59):

@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.

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:02):

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.

view this post on Zulip Rob Lewis (Jan 07 2021 at 18:03):

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

view this post on Zulip Rob Lewis (Jan 07 2021 at 18:04):

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

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:04):

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

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:05):

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.

view this post on Zulip Rob Lewis (Jan 07 2021 at 18:05):

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

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:06):

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

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:07):

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

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:08):

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

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:09):

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

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:09):

Lukas Stevens said:

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

So is gather.town :shrug:

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:10):

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

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:10):

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

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 18:11):

Is VSLiveShare easy to set up?

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:12):

I would say yes

view this post on Zulip Gabriel Ebner (Jan 07 2021 at 18:13):

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

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:13):

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

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:15):

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

view this post on Zulip Gabriel Ebner (Jan 07 2021 at 18:16):

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

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:19):

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).

view this post on Zulip Lukas Stevens (Jan 07 2021 at 18:19):

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

view this post on Zulip Sebastian Ullrich (Jan 07 2021 at 18:24):

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.

view this post on Zulip Sebastian Reichelt (Jan 07 2021 at 19:13):

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".)

view this post on Zulip Jakob von Raumer (Jan 07 2021 at 19:27):

What ITP is that built on right now?

view this post on Zulip Sebastian Reichelt (Jan 07 2021 at 19:42):

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).

view this post on Zulip Kevin Buzzard (Jan 07 2021 at 21:31):

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).

view this post on Zulip Julien Narboux (Jan 08 2021 at 07:54):

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 ?

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2021 at 07:59):

#webeditor :smile:

view this post on Zulip Bryan Gin-ge Chen (Jan 08 2021 at 08:00):

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

view this post on Zulip Julien Narboux (Jan 08 2021 at 08:04):

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.

view this post on Zulip Patrick Massot (Jan 08 2021 at 08:12):

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.

view this post on Zulip EricGT (Jan 08 2021 at 11:50):

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:


Last updated: May 08 2021 at 22:13 UTC