Zulip Chat Archive

Stream: general

Topic: Can Lean be used in jupyter notebook ?

Keyao Peng (Nov 01 2020 at 08:47):

I want to write a math lecture note, and make use of Lean. I find that the Jupyter notebook is an interactive notebook, I prefer that way.
So is it possible to embed Lean into Jupyter notebook, Just like Lean game maker(Lean game maker is good, but I don't think it's proper to write formal lecture)? Or are there other interactive notebooks support Lean?

Bryan Gin-ge Chen (Nov 01 2020 at 09:33):

It's possible in principle, but no one has written a Jupyter kernel for Lean yet. I've experimented a little bit with Lean in "Observable notebooks".

See also this post.

Last updated: Aug 03 2023 at 10:10 UTC