using Observable notebooks for teaching

Stream: Lean for teaching

[Kalle Kytölä]

For teaching math to math undergraduates with no Lean experience, I now plan to use occasional Observable notebooks with Lean tools by Bryan Gin-ge Chen. Has anyone else tried that?

What I like about those notebooks is that it is possible to write $\LaTeX$ in the markdown cells and in the editors that Bryan's tools enable. And all of this is still editable (with working Lean infoview) even by the students on their own.

The main problem I encountered is that recently the embedded Lean editors have become really really slow for me (I thought they were faster before, but might be mistaken). Custom compilations of only the necessary parts of mathlib might be an option, if I had the computer skills. I wish I understood what makes the difference in the speed of the browser-running Lean things such as playgrounds, NNGs, Gitpod, Observable, etc. It looks like some of them (at least Gitpod) are fast enough for "live use". Anyways, I guess my backup plan is to switch to VS Code for any live editing, and then copy-paste back to the notebook...

I'd be curious to hear if anyone else has used Bryan's tools for teaching!

[Kalle Kytölä]

Btw, thanks a lot @Bryan Gin-ge Chen for those awesome tools!

[Kevin Buzzard]

NNG is using lean from 2019 and I only compiled the parts of mathlib necessary for the game

[Kalle Kytölä]

Thank you! That might explain the speed difference.

Gitpod seems faster, though, even with full mathlib.

Anyways, I'm guessing that people are understandably not putting a lot of effort into optimizing teaching tools using Lean3 now. But all of these might deserve a fresh look once mathlib is in Lean4.

[Bryan Gin-ge Chen]

Glad you're finding my experiments useful! I haven't looked at them in months, so don't hesitate to let me know if I should fix something. As far as slowness is concerned, unfortunately the notebooks (and the Lean web editor) run a version of Lean directly in your browser with a significant performance penalty, so it doesn't really work well past a certain point. Gitpod runs a version of Lean on a remote server, so it's much quicker. In principle it could be possible to set up the notebooks to communicate with remote servers as well, but I didn't have the time to explore it. I did play around with connecting the notebooks to a local Lean server here but it was only a proof of concept (and I'm not sure if it still works).

If you do want to try to prepare smaller bundles for use in web editors, the instructions here should hopefully get you started. Again, feel free to ping me if you get stuck.

[Kalle Kytölä]

Thank you very much for the original Lean implementations in Observable and for the answer!

The remote server clearly explains why Gitpod is faster. I had no idea that's how Gitpod works.

I had noticed the existence of your local Lean server solution, but it still looked complicated to me. Since Lean is only a small extra component in what I will be doing in my course, I think I will not try to set up a local server this semester --- I will just temporarily switch to VS Code when necessary. (Another small advantage is that the "hover" in VS Code shows a bigger portion of the docstring than the Observable editor, so we can view the definitions and theorem statements in natural language by the hover. The biggest disadvantage of VS Code to me is the lack of LaTeX and maybe also pictures, which are available in the Observable notebook. Also Lean in VS Code would be more difficult for the students to play around with.) In any case, I really appreciate both what you have done and the offer to help with using it!

[Kalle Kytölä]

If anyone is interested in an example, in tomorrow's lecture I plan to switch to this notebook for at least half an hour. If I survive, I can let you know how it went. This is clearly rather experimental (to put it politely); having video recordings of ordinary lectures from last year is why I feel like I might not be throwing the students totally under a bus here...

[Bryan Gin-ge Chen]

Wow, good luck with the lecture! I can look into making the hover show a little more of the doc string, but making the hover pop up stick around so you can scroll it like in VS Code might be tricky...

[Kevin Kappelmann]

@Kalle Kytölä I wrote some tools around Bryan's editor some years back that will probably be useful for you https://observablehq.com/@kappelmann?tab=collections

[Julian Berman]

@Bryan Gin-ge Chen did you ever try writing a jupyter kernel for Lean?

[Alex J. Best]

Some previous discussion at https://leanprover.zulipchat.com/#narrow/stream/187764-Lean-for.20teaching/topic/tools.20for.20teaching.20with.20Lean/near/205023110

[Julian Berman]

Ah, cool.

[Julian Berman]

ipywidgets mean it may even be possible to have an embedded infoview in a notebook I suspect

[Julian Berman]

But sounds like no one's played with that yet then (and I dare not try myself until I clear some yaks off the stack)

[Patrick Massot]

If you are serious about playing with this then it may help to have a look at what William Stein did for CoCalc.

[Kalle Kytölä]

Thank you for the suggestion.

I did find lots of material by searching for William Stein on CoCalc, including some .lean-files. But I did not yet find a way to have them open in any editor. Almost surely the problem is simply that I don't know how to use CoCalc. I have so far failed to make also format_lean and Alectryon work, so no doubt this is another issue of lacking computer skills.

[Kalle Kytölä]

In the ongoing course I am serious primarily about not changing too much in the middle of it. I might be serious about using Lean in my teaching in the future, but I think sufficiently much will change with Lean4 and once I get my first data points about our students reactions to Lean that right now I'm definitely not doing much more than walking through a few Lean proofs in the lectures. Now I simply wrote Python scripts to convert LaTeX from my lecture notes to Markdown so that I can copy-paste to the Observable notebook the appropriate pieces of the notes preserving the appropriate \ref{..}s (and another script for getting the ref's in my Lean files).

I don't know if it is realistic, but I imagine after the transition to Lean4 there might be more coordinated attempts to produce teaching tools? So I'm (quite) happy to wait until then for more serious attempts.

[Kalle Kytölä]

Kevin Kappelmann said:

Kalle Kytölä I wrote some tools around Bryan's editor some years back that will probably be useful for you https://observablehq.com/@kappelmann?tab=collections

Thank you for letting me know about that! Your notebooks seem have the great feature that I was missing (or at least didn't know how to do), which is parsing code comments to LaTeX. But I will now keep things to the most straightforward option, which is just separate text/LaTeX cells and the basic version of Bryan's Lean editor.

[Kalle Kytölä]

Bryan Gin-ge Chen said:

Wow, good luck with the lecture! I can look into making the hover show a little more of the doc string, but making the hover pop up stick around so you can scroll it like in VS Code might be tricky...

Wow, I didn't know VS Code can do that! Anyways, I believe the best hover pop up size probably depends on the use case, so I don't think there are any compelling reasons to change it. I think your Lean editors work absolutely great given the constraints that mathlib is big nowadays (of which I'm very happy otherwise) and I try to run them / let the students run them on a browser. Thanks again!

[Patrick Massot]

Kalle Kytölä said:

Thank you for the suggestion.

I did find lots of material by searching for William Stein on CoCalc, including some .lean-files. But I did not yet find a way to have them open in any editor. Almost surely the problem is simply that I don't know how to use CoCalc. I have so far failed to make also format_lean and Alectryon work, so no doubt this is another issue of lacking computer skills.

About CoCalc, do you mean you can't use Lean there or you can't understand how it works under the hood? In the first case you can probably find help in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/CoCalc. About format_lean I'd be happy to help but I would need more input?

[Patrick Massot]

And in any case you are right that all this is waiting for Lean 4. There will definitely be a big surge of pedagogical material production once mathlib works with Lean 4.

[Kalle Kytölä]

About CoCalc, I did not manage to open any editor that would run anything, just raw .lean text files. So I'll check your link...

[Patrick Massot]

Opening a lean text file in CoCalc should automatically run Lean

[Patrick Massot]

I haven't tried in a very long time. Let me see if I can try

[Patrick Massot]

Do you have an account on cocalc.com?

[Kalle Kytölä]

Ah, no I don't... That must be the issue. :light_bulb:

[Kalle Kytölä]

Ok, so I'll have to look into that when I have time to create an account.

Btw, I think it is very nice that Observable does not require creating any accounts when students want to play with the notebook! At least to me that seems hugely significant. I could not expect my 144 students to create accounts, but I can expect a positive fraction of them to open a web link.

[Patrick Massot]

I just checked and there is an example project (a CoCalc project, not a Lean one) that was created three years ago to experiment with Lean in CoCalc and it still work. I think I'll be able to add you once you'll get an account.

[Patrick Massot]

But I need to go to bed anyway.

[Kalle Kytölä]

format_lean would in fact have been my original choice, but I failed to set it up. There was an error message of which I did not know what it was trying to tell me. I think I'm interested in learning about that in the future, thanks for the offer to help! But now I think I will stick to the current setup --- and I'll let you get sleep! :smile:

[Patrick Massot]

I'm really sorry I missed that question. Next time you should insist until I write something.

[Kalle Kytölä]

No worries! This is my first experiment incorporating any Lean aspects in teaching. I hope it won't be the last. :smile: