xeus-lean: A Jupyter kernel with the main loop in Lean 4

Stream: lean4

[junji hashimoto]

Hi everyone,

I'm excited to share a project I've been working on: xeus-lean https://github.com/Verilean/xeus-lean

It is a Jupyter kernel for Lean 4 based on the xeus protocol. The key characteristic of this implementation is that the main loop and kernel logic are implemented in Lean 4 itself (binding to xeus via FFI), rather than wrapping Lean from C++.

This serves as a proof-of-concept for:

1. Using Lean 4 for system-level programming and complex C++ interoperability.
2. Creating interactive environments purely within the Lean ecosystem.

Future Roadmap: My ultimate goal involves compiling this kernel to WebAssembly (WASM). This would enable Lean 4 to run entirely in the browser via JupyterLite, providing a zero-setup, interactive learning environment for tutorials and textbooks without backend servers.

I hope this helps anyone looking to run Lean 4 in Jupyter notebooks. Feedback and contributions are welcome!