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.
• 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.

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 syntax highlighting in the WebUI, currently it sees Lean 4 as Python
• 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.

Getting started

Prerequisites

1. You need a working Lean 4 installation. You can install it via elan, e.g. on Linux-like systems:

curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | bash -s -- -y --default-toolchain none

2. You need a working Python (e.g. 3.11). If you prefer to use a virtual environment, you need to activate it before installing the kernel.

Installation script

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.

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

To use it, run one of:

# Web UI
jupyter notebook
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

First, verify that lean and lake is 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.

Then, you need to have 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.

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

Then, ensure that you have python, pip installed, and install Jupyter:

pip install notebook
# or
# pip install jupyterlab

Then, install the kernel:

# Option 1: Install from PyPI
# see "Support matrix" for the tested versions
pip install lean4_jupyter
# Option 2 (recommended): install the latest version from the repo
pip install git+https://github.com/utensil/lean4_jupyter.git
# or in development mode, check out the repo then run
# pip install -e .
python -m lean4_jupyter.install

To use it, run one of:

# Web UI
jupyter notebook
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

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.

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