Zulip Chat Archive

Stream: Lean for teaching

Topic: tools for teaching with Lean

Alexandre Rademaker (Jul 25 2020 at 21:53):

I woud like to have tips from people using Lean during courses. I will start a course on discrete mathematics using Lean and I am looking for tools to:

  1. assignments and self-grade. GitHub Classroom provides some functionalities, anyone here has used it? Alternatives? Sites like https://repl.it?
  2. user-friendly interfaces for the students: many are now very comfortable with notebooks like Jupyter, does anyone tried to make a kernel for Lean in Jupiter?

Bryan Gin-ge Chen (Jul 25 2020 at 22:02):

  1. Not to my knowledge. I'd be happy to help anyone who wanted to start such a project though.

Bryan Gin-ge Chen (Jul 25 2020 at 22:05):

I guess one would first have to decide how to translate the "execution" of Jupyter notebook cells into something compatible with how the Lean server processes Lean files. I played around with embedding Lean in a different kind of notebook, but I think a lot more experimentation in this space is needed.

Bryan Gin-ge Chen (Jul 25 2020 at 22:10):

Presumably a good starting point for writing a Lean kernel for Jupyter would be @Patrick Massot and @Jason Rute 's lean-client-python.

Alex J. Best (Jul 26 2020 at 03:36):

There is a coq jupyter notebook, might be good to look at that if anyone takes this on.

Last updated: Dec 20 2023 at 11:08 UTC