Can Lean be used in jupyter notebook ?

Stream: general

[Keyao Peng]

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]

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.