lean4_jupyter

A Lean 4 Jupyter kernel via repl.

Features

🔥 See it in action: Tutorial notebook.

The kernel can:

• execute Lean 4 commands (including definitions, theorems, etc.)
• execute Lean 4 tactics with magic like % proof immediately after a sorryed theorem
• backtrack to earlier environment or proof states with magic like % env 1 or % prove 3
• support magics like %cd or %load (loading a file)
• support for importing modules from projects and their dependencies, e.g. Mathlib ( demo ).

Output:

• In jupyter notebook and alike:
  • echos the input annotated in alectryon style, at the corresponding line (not columns yet), with messages, proof states etc.
  • highlights Lean 4 syntax in code cells via a companion JuptyerLab extension jupyterlab-lean4-codemirror-extension
• In jupyter console and alike: echos the input annotated in codespan style, at the corresponding line:column, with messages, proof states etc.
• Raw repl input/output in JSON format can be inspected by click-to-expand in the WebUI.

The kernel code is linted by flake8, and tested with nbval in CI.

Getting started

Prerequisites

1. A working Lean 4 installation. You can install it via elan.

2. A working Python installation (e.g. 3.11). If using a virtual environment, activate it before installing the kernel.

One-liner installation

The following script will install a repl of a compatible Lean 4 toolchain, the kernel, and prepare the demo Lean 4 project.

git clone https://github.com/utensil/lean4_jupyter.git && cd lean4_jupyter && ./scripts/prep.sh

Note: the script could remove an existing repl, and it assumes /usr/local/bin is in your PATH, it will also set the default Lean 4 toolchain to the same as the one used by the repl to ensure repl works outside projects. For installing the extension to highlight Lean 4 syntax in JupyterLab, it will also use nvm to install Node.js if it's not installed.

If you prefer manual installation, please read Manual installation below.

The installation script creates a virtual environment in the .venv folder in the repo, and installs the kernel into it. You can activate the virtual environment with:

source .venv/bin/activate

Then use jupyter as usual.

Usage

To use it, run one of:

# Web UI

# classic notebook
jupyter notebook
# JuptyerLab (recommended)
jupyter lab

# Console UI

# hint: use Ctrl-D and confirm with y to exit
jupyter console --kernel lean4
# hint: you need to run `pip install PyQt5 qtconsole` to install it
jupyter qtconsole --kernel lean4

then open notebooks in the examples folder to familiarize yourself with the basic usage.

Manual installation

1. Verify that lean and lake are in your PATH:

lean --version
lake --help|head -n 1

they should output Lean/Lake versions, respectively. If not, you can install them via elan.

2. Install a working repl in your PATH.

You can build it from source (please read and adjust them before executing) using the example script scripts/install_repl.sh.

3. Verify that repl is working:

echo '{"cmd": "#eval Lean.versionString"}'|repl

In case repl hangs, you could kill it with

ps aux|grep repl|grep -v grep|awk '{print $2}'|xargs kill -9

4. Ensure that you have python, pip installed, and install Jupyter:

pip install notebook
# or
# pip install jupyterlab

Install the kernel using one of these options:

# Option 1: Install from PyPI (see "Support matrix" for tested versions)
pip install lean4_jupyter

# Option 2 (recommended): Install latest version from repo
pip install git+https://github.com/utensil/lean4_jupyter.git

# Option 3: Install in development mode (after checking out repo)
# pip install -e .

# After installing, register the kernel
python -m lean4_jupyter.install

Verify the kernel installation with:

jupyter kernelspec list

(Optional) Installing the JupyterLab Extension

If you are using JupyterLab, you can install the JupyterLab extension to enhance your experience with Lean 4 syntax highlighting for code cells:

1. Ensure Node.js is installed (version 22.0.0 or higher):

node -v

2. Install Python dependencies:

pip install ipykernel jupyterlab jupyter_packaging

3. Clone the repository (if not already done) and install the extension:

git clone https://github.com/utensil/lean4_jupyter.git
cd lean4_jupyter/ext
jlpm install
jlpm build
pip install .
jupyter-labextension install .

4. Verify the installation:

jupyter-labextension list

Rationale

I've always wanted to do literate programming with Lean 4 in Jupyter, but Lean LSP and Infoview in VS Code has provided an immersive experience with immediate feedback, so I could never imagine a better way to interact with Lean 4, until interacting with repl makes me believe that limitless backtrack is another feature that best accompanies the reproducible interactivity of alectryon style annotations.

The idea came to me in an afternoon, and I thought it's technically trivial to implement overnight thanks to repl. It took me a bit longer to work out the logistics of UX and polish the code, but it's fun to see the potential.

This also serves as a human-friendly way to understand how Lean 4 repl works, for integrating repl with ML systems.

What's next

• Add support for Quarto, possibly integrate with Molten in Neovim
• Add support for Incrementality, see also repl#57
• Make use of Goal State Diffing
• Improve the alectryon annotation to support annotations in the middle of a line
• Provide a switch to use codespan instead of alectryon in the WebUI, or a way to see warnings and errors without hovering or clicking
• Provide a switch for raw repl input/output inspection as a magic, disable it by default
• Learn from previous prototypes to improve UX
• Make magics like %cd and %load work more robustly
• Support show tactics after %load
• Add all repl test cases to the CI and set up coverage
• Improve UI in Jupyter Dark themes
• Support running lake commands via %lake, e.g. %lake build
• Better (streamed) feedback for long running commands such as import
• Support changing Lean toolchain and adding dependencies in an ad hoc manner
• Minimize emmitted HTML code
• Possibly use @shikijs/twoslash style annotation and no longer depends on alectryon
• Possibly change to Aya style annotation for plain text output
• Minor code refactor to smooth things out

If you are interested in one of these TODOs, or you have some other nice features in mind, you may raise the discussion by opening an issue or discuss it in the Zulip topic.

Inspired by

• Making simple Python wrapper kernels
• bash_kernel
• pySagredo (see also repl#5)
• LeanDojo
• alectryon
• codespan
• lean-lsp (My previous attempt to make a Lean 4 Jupyter kernel using Lean 4 LSP server)

Support matrix

lean4_jupyter	Tested Lean 4 toolchain	Tested Python version
0.0.1	v4.8.0-rc1	3.11.0
0.0.2	v4.11.0	3.11.0
0.0.3-dev (git main)	v4.11.0	3.13.0 (jupyterlab: 4.3.0)