Interactive Lean videos

Stream: Lean for teaching

[Yuri Sulyma]

Hi, first time in this server. As I mentioned in #new-members, I've developed software for making interactive videos for teaching. "Interactive" means students can e.g. run code inside the video, or manipulate graphs inside the video (examples below).

I would like to add support for recording interactive Lean tutorials. As a first step, it would be helpful for me to chat with someone who:

• is very familiar with lean4web / interacting with a Lean server programmatically
• has experience deploying a Lean server to a cloud environment like AWS

It would also be great to hear from folks interested in recording such videos themselves.

Examples:

• https://epiplexis.xyz/old/insertion-sort seek to 9:29; the Playground tab is a buffer where you can edit and run your own Python code, while Copy will copy the code I wrote into the playground. The Lean recording
• https://www.math.brown.edu/ysulyma/f21-math180/14/6.html you can rotate the scenes and drag the red point with your mouse/finger

[Jeremy Avigad]

The examples are nice! I am looking forward to seeing what comes of this. Good luck with it.

[Alexander Bentkamp]

Sent you a DM!