A Jupyter kernel for Lean 4 based on the xeus framework. Runs both as a native desktop kernel and as a WASM kernel in the browser via JupyterLite — so a reader can try Lean without installing anything.

⚠️ What this project is, and isn't.

This is a playground. The goal is to let curious people read a chapter, click into a cell, and feel what writing a small Lean definition or formal statement is like — all from inside a browser tab.

It is not a substitute for the proper Lean development environment. If you want to do real proof work — interactive infoview, gutter diagnostics, term-mode hovers, tactic suggestions, project-wide elan/lake — install VS Code with the Lean 4 extension and follow that path. The browser build trades depth for zero-install reach.

So: don't expect VS Code parity. Don't file bugs about missing lean --print-prefix ergonomics. Treat this as the "free trial" that gets a reader hooked enough to install the real thing.

• Read tutorials with pictures and runnable cells side-by-side.
• Press Shift+Enter on a cell, see Lean evaluate it.
• Modify the cell and re-run it. State carries from cell to cell.
• Optional: load Mathlib chunks on demand with %load mathlib and try Mathlib theorems live.

What not to expect in the browser kernel:

• Interactive goal-state infoview (use VS Code).
• Project-wide refactoring or lake-aware diagnostics (use VS Code).
• A "Save" that round-trips to your repo (the JupyterLite filesystem is a single-tab IndexedDB; export your notebook to download it).
• Performance parity with native (the WASM kernel uses ~2 GB per tab and takes seconds for a cold boot).

Click into the live site:

→ https://verilean.github.io/xeus-lean/lab/index.html

There's a starter notebook, a small Mathlib demo (run %load mathlib in the first cell, then import Mathlib.Tactic), and the function-language tutorial pre-loaded.

If you want to learn Lean as a programming language before touching proofs, jump to the function-language tutorial and skim Ch00–Ch16.

If you want to see what Lean + Mathlib feels like for math, open docs/math-visual/ and start with the complex analysis Ch01. Those chapters are deliberately Needham-style: a picture, some numerical play, then the formal Lean statement.

If you want to put the same JupyterLite experience behind your own URL — for a class, a workshop, or to bundle a different Mathlib snapshot — there are three reasonable paths.

The simplest path: serve the prebuilt site under your own domain without re-running the WASM build.

1. Clone the live deployment branch:

   git clone --branch gh-pages https://github.com/verilean/xeus-lean.git xeus-lean-site

2. Serve xeus-lean-site/ with any static HTTP server. The whole site is a couple of GB; serve it from a CDN (Cloudflare Pages, Netlify, Vercel) or any HTTP host that can serve files up to ~1.3 GB (the largest Mathlib chunk).

   cd xeus-lean-site
   python3 -m http.server 8000   # or your favourite static server

3. Open http://localhost:8000/lab/index.html. That's it — the kernel is entirely client-side, your server only delivers files.

If you want to bundle your own additions (custom notebooks, your project's Lean lib, a Mathlib snapshot pinned to your toolchain), build the JupyterLite site locally and serve it the same way.

git clone https://github.com/verilean/xeus-lean
cd xeus-lean

# WASM build with Mathlib (slow: 30-60 min on a fast laptop)
make docker-e2e-image-with-mathlib

# The built site lives in the image under /work/_output
docker run --rm -it -p 8765:8765 --name xeus-serve xeus-lean-e2e \
  bash -c 'cd /work/_output && python3 -m http.server 8765'

Visit http://localhost:8765/lab/index.html.

To bundle your own notebooks, drop them into notebooks/ before building; the WASM Dockerfile copies that directory into the jupyter lite build --contents step.

The _output/ from option B is a plain static site. Any of:

• GitHub Pages: push the _output/ content to a gh-pages branch. Caveat: Mathlib chunks exceed GitHub's 100 MB single-file warning; for full Mathlib hosting you'll want a CDN-backed origin.
• Cloudflare Pages / Netlify / Vercel: upload _output/ as the publish directory. Configure the Cross-Origin-Embedder-Policy / Cross-Origin-Opener-Policy headers if you need SharedArrayBuffer (xeus-lean's WASM build doesn't require it today, but JupyterLite some extensions do).
• S3 / GCS / any object store: serve as a website bucket.

No runtime backend is needed. The entire Lean kernel — runtime, Mathlib oleans, JupyterLite shell — is downloaded once and runs in the user's tab.

Mathlib oleans are split into per-namespace chunks (Mathlib.Algebra, Mathlib.Topology, …) under _output/xeus/wasm-host/olean/ so a tab can fetch only what its notebook actually uses (%load mathlib triggers the fetches on demand). Total bundle size with all chunks: ~1.7 GB compressed. Total size of the default-no-Mathlib site: ~280 MB compressed.

• Rich display in cells — Display.html, Display.latex, Display.svg, Display.markdown, Display.bv, Display.verilog, Display.waveform, Display.blockDiagram, Display.mermaid.
• Notebook helpers — #help_x lists registered commands; #findDecl / #listNs / #sig search the env; #bash, #mermaid, #savefig.
• Comm protocol on the WASM side — used for interactive widgets like the waveform viewer.
• Docs pipeline — docs/Convert.md: one Markdown source → .ipynb, runnable .lean:percent, a static HTML site, or evaluated-output-baked Markdown.
• MCP server (xlean-mcp) — a stdio Model Context Protocol server so a local agent (Claude Code, etc.) can drive the kernel programmatically. See the next section.

xlean-mcp is an MCP 2024-11-05 server that exposes Lean evaluation, notebook editing, and project-search operations to any MCP-compatible host. Build it once and point your host at it:

lake build xlean-mcp
# binary lives at .lake/build/bin/xlean-mcp

Tools in v0.2 (tools/list returns them in the order below):

Wire it into Claude Code by adding the binary to your MCP config:

{
  "mcpServers": {
    "xlean": {
      "command": "/abs/path/to/xeus-lean/.lake/build/bin/xlean-mcp"
    }
  }
}

Then in chat:

Read notebooks/mathlib-demo.ipynb, change the third cell to import Mathlib.Tactic.Ring, and write it back.

The agent can read the file, edit the cell, write it back, and verify the result — all without leaving the protocol.

Caveats — this is v0.2:

• lean_eval shells out to a fresh lean per call; no environment carries between calls (definitions in one call aren't visible in the next). Sharing the REPL env across tool calls is on the roadmap (#63).
• project_search runs in the server's working directory, which is whatever the MCP host launched it from. If you want a specific workspace root, launch the server from there.
• No tools yet for the running browser JupyterLite session — that needs a service-worker shim in the WASM site (#64).

Native:
  Jupyter Client ──ZMQ──▶ Lean Main (XeusKernel.lean)
                               │  FFI
                          C++ xeus (xeus_ffi.cpp)

WASM (in-browser, no server):
  Browser tab ──Web Worker──▶ xlean.js + xlean.wasm (Memory64)
                                   │
                              Lean runtime, single-threaded
                                   │
                              MEMFS populated from .tar.zst
                              chunks fetched on demand
                              + IndexedDB cache for warm boots

For the kernel internals — the five WASM bottlenecks we hit, the env-reuse workaround, the per-module zstd tarball pipeline — see WASM_BUILD.md. For Mathlib loading, see the comments inside src/post.js.

What goes in this repo, and what doesn't.

The xeus-lean repository owns three things:

1. The Lean WASM/native kernel (xlean, xlean.wasm/js) and its REPL frontend.
2. The JupyterLite hosting glue (pre.js, post.js, manifest loader, %load, %memory).
3. A vendor-agnostic mechanism for downstream Lean libraries to plug their own static archives, Lean externs, and oleans into both build targets (WASM and native).

What it does not own: any particular third-party library. Sparkle, Hesper, Mathlib bundle assemblers, future Lean libraries — all of those live in their own repos and use the extension point below. No third-party project name should appear in xeus-lean's build files (CMake / Dockerfiles / CI workflows / Lean REPL boot).

If you find such a name in this repo, file an issue — it's a bug, not a feature.

The WASM build accepts a CMake variable EXTRA_WASM_DIRS — a ;-separated list of staging directories produced by third-party projects. Each staging directory must contain a manifest:

// <staging>/xeus-lean-extra.json
{
  "archive":    "lib/libmylib_wasm.a",      // whole-archive into xlean
  "exports":    "lib/mylib_exports.txt",    // one C symbol per line
  "olean_root": "MyLib"                     // optional; copied to /lib/lean/
}

The third-party project's build script writes those three artefacts into <staging>/lib/ + <staging>/MyLib/** and emits the manifest. xeus-lean's CMake then:

1. Whole-archives libmylib_wasm.a into xlean.wasm (Lean externs would otherwise be DCE'd).
2. Splats mylib_exports.txt into emcc's -sEXPORTED_FUNCTIONS so the symbols survive LTO.
3. Copies MyLib/**/*.olean into the JupyterLite olean asset tree alongside Init/Std/Lean/Mathlib.

Pass it to the WASM build like so:

emcmake cmake -S . -B wasm-build \
  -DEXTRA_WASM_DIRS="/path/to/mylib-staging;/path/to/otherlib-staging"

The repo ships a minimal third-party-style fixture under tests/fixtures/mock-extra/ that exercises the whole extension path: a MockExtra Lean lib with @[extern "mock_hello"] opaque mockHello, a C file implementing it, a build-wasm.sh that emits the manifest, and a CI step that links it via EXTRA_WASM_DIRS and asserts #eval mockHello () returns the expected string.

That fixture is the contract. If you can write a downstream lib that plugs in the same way, you're done. If EXTRA_WASM_DIRS ever breaks, the fixture's CI step turns red.

The Lean WASM build itself takes ~30 minutes from cold (Lean runtime, REPL, xeus glue, emcc link). We do not want every downstream consumer to pay that cost just because they're adding a 1-MB extra library. The plan to avoid it:

So stage 1 proves correctness (the third-party path works); stage 2 proves it's also fast enough for downstream consumers to use without their own CI grinding. Both stages preserve the rule that xeus-lean itself never knows a third-party name.

Same story is in progress for the native xlean binary (dlopen of shared libraries declared via a sibling manifest). Not yet wired — tracked separately so the WASM contract lands first.

GitHub Actions builds both targets on every push:

• Native: Linux x86_64, uploads xlean binary
• WASM: emscripten Memory64, runs test_wasm_node, deploys JupyterLite to GitHub Pages

Apache License 2.0.

• xeus — Jupyter kernel protocol framework, by QuantStack.
• Lean 4 REPL — the basis for src/REPL/, by the Lean community.
• JupyterLite — the in-browser Jupyter runtime that hosts the WASM kernel.
• Mathlib — the formal-math library; the per-namespace chunks under xeus/wasm-host/olean/Mathlib.*-olean.tar.zst come from Mathlib's build for our pinned Lean toolchain.