tools for teaching with Lean

Stream: Lean for teaching

[Alexandre Rademaker]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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