Browser Lean

Run Lean 4 entirely in the browser — no server, no upload, no install. The real Lean elaborator and kernel are compiled to WebAssembly, so a proof typed into the page is checked in that tab, on your machine.

This is a proof of concept for adding a lean language to LiveCodes, in the same shape as browser-cobol, browser-haskell and browser-elixir were for their languages.

It is fast enough to use: the runtime is ready ~2.2 s after the first Run, and a proof is checked in ~0.3 s.

Lean 4 source
  → real Lean 4 (cauli/lean4 `reinstate-wasm` fork, wasm32)   elaborate + kernel-check
  → JSON messages, one per line, on stdout                    severity: information | error
  → the page splits them by severity                          output / diagnostics

The runtime lives in a persistent Web Worker that imports Init once and then compiles repeatedly through the fork's lean_wasm_compile export, reusing the environment it has already imported. The library ships as 5 packed gzip files (629 modules, 1,887 .olean/.ir files) rather than ~1,900 individual requests.

The Lean WASM artifacts are built by cauli/lean4-wasm-in-browser (Apache-2.0) — the reference implementation for this, and the source of the worker's structure and the boot sequence. Credit for making Lean run well in a browser belongs there.

Demo

npm run assets          # mirror ~127 MB of Lean artifacts into public/lean-wasm/ (once)
npm run assets:libs     # optional: Std/Lean/Batteries for lazy imports (~377 MB)
npm run assets:mathlib  # optional: the Mathlib layer (~316 MB compressed)
npm start               # → http://localhost:8129/
# or, once wasm-build/out/mirror-upstream is assembled, the single-threaded mirror:
npm run start:canonical # → http://localhost:8129/?baseUrl=http://localhost:8131

Pick an example (or type your own), press Run — or Ctrl/Cmd + Enter in the editor. Nothing is downloaded until the first Run.

No cross-origin isolation

The page needs no Cross-Origin-Opener-Policy, no Cross-Origin-Embedder-Policy, and no SharedArrayBuffer. The canonical artifact is a single-threaded build: with no pthreads the linker never demands a shared memory, and the module defines an unshared one (flags=1, shared=false). That is what npm run start:canonical serves — page on 8129 without isolation headers, mirror on 8131 — and the demo accepts proofs on it, verified in Chrome and Firefox. See FINDINGS.md §9.7 and §9.8 for the build and its measurements.

The requirement belongs to the artifact, not to the page, and the runtime reads which it is off the wasm rather than trusting a global: the first 64 KiB are enough to parse the memory section, whose limits flags decide everything (flags 3 is has-max | shared). A shared artifact is therefore refused before the 16.5 MiB of wasm is fetched, and the page names it:

The Lean artifact at …/lean.wasm.gz declares a shared WebAssembly memory, so it needs
SharedArrayBuffer — which a document only has when it is cross-origin isolated. …

The upstream pthread artifact still needs isolation, which is what the stricter npm start — COOP/COEP by default — is for. Chrome also offers two ways to skip the headers: a reverse origin trial for SharedArrayBuffer, which has been extended more than once and sits on a deprecation path, and Document-Isolation-Policy, which isolates a document for itself, applies per frame, and shipped in Chrome 137 for desktop. Both are Chrome-only, and the point of the single-threaded build is that neither is needed. See FINDINGS.md §2.

To see a proof checked with no headers at all:

npm run start:no-isolation   # same page, no COOP/COEP — and it still compiles

What you get

• Client-side checking. Nothing is uploaded; the verdict on your proof comes from a wasm module in the tab.
• Real diagnostics, with positions — error: Tactic \rfl` failed: The left-hand side 1 is not definitionally equal to the right-hand side 2/⊢ 1 = 2 (line 1, col 32)`.
• #eval, #check, #print, user-defined recursion, and #eval of library functions — #eval (List.range 5).map (fun n => n * n) prints [0, 1, 4, 9, 16].
• Core tactic proofs (induction, rw, simp).
• A clean split between program output and diagnostics, even though the runtime puts both on stdout (FINDINGS.md §3).
• Lazy loading: the page is three small files; the 127 MB of artifacts wait for the first Run.

Verified

Each row was run through the page in headless Chrome and the panes read back.

snippet	output	exit	run
#eval "Hello from Lean!"	"Hello from Lean!"	0	—
#eval 2 + 2, #eval 2 ^ 10, #check Nat.add_comm	4, 1024, Nat.add_comm (n m : Nat) : n + m = m + n	0	—
def fib + #eval fib 10 / #eval fib 20	55, 6765	0	0.28 s
theorem add_comm … := by induction b with …	accepted, no diagnostics	0	0.28–0.67 s
#eval (List.range 5).map (fun n => n * n)	[0, 1, 4, 9, 16]	0	0.08 s
#check this_is_not_defined	error: Unknown identifier \this_is_not_defined` (line 1, col 6)`	1	0.01 s
theorem t : (1 : Nat) = 2 := by rfl	error: Tactic \rfl` failed: … (line 1, col 32)`	1	0.03 s
def broken : Nat := (a parse error, with the Lean library loaded)	error: syntax error at line 2, column 0	1	0.01 s
import Std.Data.HashMap + #eval a HashMap fold	[(1, 1), (2, 2), (3, 3)]	0	0.20 s
import Lean + #eval (Name.mkSimple "hello").toString	"hello", Lean.Expr : Type	0	0.02 s
import Batteries	accepted	0	5.5 s first time, then 0.1 s
import Mathlib.Data.Real.Basic + Mathlib.Tactic.Ring, example (x : ℝ) : x + 0 = x := by ring	accepted, #check Real → Real : Type	0	10.4 s first time, then 2.6 s
Mathlib.Tactic.NormNum + Linarith proofs on ℚ and ℝ	accepted	0	2.6 s (warm)
import Mathlib.Analysis.SpecialFunctions.Sqrt (outside the closure)	object file '…/Sqrt.olean' … does not exist + a note	1	0.2 s

Runtime ready in 2.2 s. Compiles are milliseconds to a few hundred milliseconds, and get faster as the imported environment is reused.

Capability handling was checked in every configuration that matters — three the host can present, and the artifact kind that is the point of all this:

served as	SharedArrayBuffer	behaviour
the canonical build, no headers (npm run start:canonical)	absent	boots and checks proofs — the configuration this repo exists for
the canonical build, with COOP/COEP (npm start)	present, isolated	boots; the headers change nothing for it
the shared (pthread) build, no headers	absent	refuses, naming the artifact and both remedies — before the boot, so the 16.5 MiB artifact is never fetched
the shared build, simulated origin trial (global present, document not isolated)	present, not isolated	attempts to boot, and reports a stalled boot rather than hanging

Assets

asset	bytes
lean.wasm	100,838,905 (96.17 MiB)
core layer, 5 packs (629 modules, 1,887 files)	32,184,975 (30.69 MiB)
core-layer.json	313,732
lean.js	148,402
on disk	~127 MiB

Over the wire it is far less: the wasm is brotli-compressed in transit (96.17 MiB → 16.1 MB), and the packs are already gzip, so a first load transfers roughly 47 MB.

Storing it is the other problem, and it is one file. Cloudflare Pages refuses anything over 25 MiB, and lean.wasm is 96.2 MiB — every other file in the mirror is small. npm run assets therefore has a compressed variant: gzipped the wasm is 16.5 MiB (5.82×; brotli reaches 8.9 MiB but DecompressionStream cannot read it), and the per-file library tree falls from 376.8 to 143.1 MiB, taking the whole mirror from ~823 MiB to ~490 MiB with nothing over the limit. The runtime decompresses in the browser, so the host needs no special headers beyond the two below. It also checks what it fetches: these hosts answer 200 with an HTML shell for files they do not have, which surfaces much later as failed to read file '…', invalid header (FINDINGS §5).

npm run assets mirrors the pinned build. The artifacts are not committed; they are fetched from a third-party deploy because they cannot be hotlinked — see FINDINGS.md §5, which also explains why the version must be pinned (?v=) and how a mismatch shows up.

npm run assets:libs separately mirrors the optional libraries used by lazy imports: 5,598 files, ~377 MiB, being .olean + .ir + .ir.sig for each of 1,866 modules (Std, Lean, Batteries).

npm run assets:mathlib mirrors the Mathlib layer: real-analysis-layer.json plus 52 packs, 316.3 MiB compressed (809.8 MiB once installed — 12,909 files, 4,303 modules).

Libraries

Init is always available. Std, Lean (metaprogramming) and Batteries are loaded on demand — write the import and it works:

import Std.Data.HashMap

def counts (xs : List Nat) : Std.HashMap Nat Nat :=
  xs.foldl (fun m x => m.insert x ((m.getD x 0) + 1)) {}

#eval (counts [1, 2, 2, 3, 3, 3]).toList   -- [(1, 1), (2, 2), (3, 3)]

When Lean reports a missing module the page fetches that library, installs it into the virtual filesystem mid-session and recompiles — so the first use of a library costs a fetch and every run after it is milliseconds. Nothing is loaded unless you import it.

The closure is discovered by asking the compiler rather than by parsing .olean dependency headers: Lean's unknown module prefix 'X' names exactly what is absent, so the page loads X and tries again. import Batteries therefore pulls in whatever Batteries itself needs.

Imports are read from your program, so the number of imports does not multiply the work: eight imports from Std cost one load and one compile, not eight. Only transitive dependencies need extra rounds, and there are only three libraries to discover, so a program is never more than a few rounds from working. Measured: 8 imports across the three libraries → 1 compile; import Batteries alone on a cold page → 3 compiles (Batteries → Lean → Std).

Upstream ships these as individual files, not packs — lean-lib-files.json indexes 2,658 modules and there is no std-layer.json, because packing is a startup optimisation for the Init closure only. npm run assets:libs mirrors that tree for the three libraries (5,598 files, ~377 MiB, gitignored).

Mathlib works — as a 4,303-module closure. Upstream publishes Mathlib only as a packed layer, the closure its Real Analysis game needs, so npm run assets:mathlib mirrors it (~316 MiB compressed, 809.8 MiB installed) and this works:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic.Ring

example (x : ℝ) : x + 0 = x := by ring

norm_num and linarith work too. Two things to know:

• There is no umbrella Mathlib module. import Mathlib alone is not a Lean module and never was — import specific ones, as you would in a Lean project.
• It is a closure, not all of Mathlib. Mathlib.Analysis.SpecialFunctions.Sqrt, for example, is not in it. A module outside the closure fails with object file '…' of module … does not exist, and the page notes that this is the published closure rather than a mistake. Upstream deliberately does not ship full Mathlib: a complete environment snapshot was tested and rejected because compaction exceeded the practical wasm heap.

Snapshots: the first run, not the import

The canonical mirror ships four --incr-header-save environment snapshots under lean-wasm/snapshots/, baked by the artifact against the library tree the mirror serves, and gzipped because they compress ~2.4×:

snapshot	raw	gzipped	first run
init (no imports)	71.1 MB	28.6 MB	0.37 s
std (Std.Data.HashMap)	109.4 MB	46.0 MB	6.0 s
lean (import Lean)	313.1 MB	128.8 MB	9.8 s
mathlib (Real.Basic + Tactic.Ring)	408.0 MB	168.8 MB	184.7 s

The runtime probes snapshots/<name>.snap.gz first and falls back to <name>.snap, so a host may serve either layout. A snapshot's cache key is the header's import list, so one exists per header and no snapshot covers a program with different imports; a run without one simply pays the import (Lean 137 s, Mathlib 605 s). Bake with node --stack-size=4000 wasm-build/bake-snapshot.cjs … against wasm-build/out/bake-lib, not the artifact's own tree — the difference is a 40-byte .olean githash and it is the difference between saving and dying in the serializer (FINDINGS.md §9.15).

Without the mirrors these imports fail with a note naming the command to run — npm run assets:libs for Std/Lean/Batteries, npm run assets:mathlib for Mathlib. See FINDINGS.md §5.

Limitations

• Syntax errors are caught only once the Lean library is loaded. The runtime's compile entry swallows parse errors entirely (FINDINGS.md §6.1), so the page hands your source to Lean's own parser — and that parser lives in the Lean library. By default the check therefore runs only when the library is already loaded for another reason (import Lean, or Mathlib), which keeps the default page at ~127 MB; in a session that never loads Lean, a typo still passes silently. ?syntaxCheck=full always checks (paying ~350 MB for the libraries), ?syntaxCheck=0 turns it off.
• Mathlib here is a 4,303-module closure, not Mathlib. Some modules (Mathlib.Analysis.SpecialFunctions.Sqrt) are absent; the page says so when you hit one. There is no umbrella Mathlib module either.
• The Mathlib layer is heavy: ~316 MB to mirror and 809.8 MiB installed once loaded, on top of the other libraries. It is fetched only when something imports it.
• The optional libraries need their own mirror. Without npm run assets:libs or npm run assets:mathlib, the corresponding imports fail with a note naming the command to run.
• Isolation belongs to the artifact, not to the page. The canonical build declares an unshared memory and needs none; the upstream pthread build does, and a stub SharedArrayBuffer does not help it — unlike the trick browser-cobol documented — because that runtime really constructs one for its pthread pool, so a fake passes the type check and then wedges the boot. The runtime reads the requirement off the wasm before booting either way (FINDINGS.md §9).
• A stalled boot is reported, not hung on. If the module instantiates but never finishes starting, the page fails after 60 s of silence with an explanation instead of sitting on "loading" forever.
• No way to interrupt a non-terminating elaboration; recovery is a page reload (~2 s).
• The canonical mirror is large: ~1.0 GiB static (1,027 MiB), of which 372 MB is the four gzipped snapshots and 331 MB the compressed Mathlib layer. The demo's core-only mirror is ~127 MiB.
• Chrome is measured; Firefox works. Safari and mobile have not been exercised.

Closer to a LiveCodes language

The reason this was not shippable has changed, and it is worth restating because the earlier conclusion was correct at the time. A LiveCodes result page runs in a sandboxed iframe inside someone else's document and cannot give itself COOP/COEP, which ruled out any runtime that needs cross-origin isolation; the only escape was a Chrome-only one (FINDINGS.md §2). That is no longer the blocker:

• A single-threaded build exists — wasm-build/ builds it, its memory is unshared (flags=1, shared=false), and this page accepts proofs on it in a document that is not isolated at all (FINDINGS.md §9.7).
• The runtime already handles both artifacts and decides from the wasm itself, so the same page serves either with no configuration.
• The pthread build still needs isolation, whatever Chrome 155 will do with a shared memory: measured, a non-isolated page stalls it (Starting the Lean runtime timed out after 120s), because Emscripten's glue gates threading on the SharedArrayBuffer global. So the single-threaded build is the only one that runs headerless at all. Its Init import is no longer a cost on the user's path: the mirror's snapshots take the first run to 0.37 s (FINDINGS.md §9.7, §9.15).

What is left before a lean language is not a wall but work: host the mirror (artifact, layers and snapshots as one versioned unit), exercise Safari and mobile (Chrome is measured and Firefox works, and the atomic-instruction question lives in the untested engines), and choose between the two artifacts. With the four snapshots the single-threaded one no longer pays 54 s on its first compile — Lean is 9.8 s and Mathlib 184.7 s — while the pthread one still needs isolation on engines that insist on it.

npm package

packages/lean-wasm is @live-codes/lean-wasm — the same runtime as a library, in the shape the other @live-codes/* language packages take: an ES module entry, an IIFE build for classic workers (which is how LiveCodes loads a language's driver), and lean-wasm-fetch-assets to materialise the assets for a host you control. It ships code only (~34 kB) because Lean's wasm is a single 96.2 MiB file and jsDelivr refuses files over 20 MB — the assets can never travel in a tarball.

See packages/lean-wasm/README.md.

Layout

public/index.html      the page: examples, editor, output, diagnostics, log
public/main.js         the demo's UI only — it drives the package below, and owns no driver logic
public/vendor/         the package's browser build, vendored by `npm run sync:vendor` (committed)
public/_headers        COOP/COEP for Cloudflare Pages, which is how a static host gets isolation
packages/lean-wasm/    the published package, `@live-codes/lean-wasm`
  worker/lean-worker.js    the Lean runtime host (adapted from upstream, Apache-2.0) — a build input
  src/                     the compiler, asset resolution, message classification, syntax probe,
                           and the artifact probe that reads the memory mode off the wasm
  bin/fetch-assets.mjs     the asset CLI (`npm run assets`), which also writes compressed layouts
  dist/lean-wasm.global.js the IIFE build, which is what gets vendored
wasm-build/            the harness for a single-threaded build, and why it is upstream work (FINDINGS §9)
serve.js               static server: COOP/COEP on by default, and nothing else
FINDINGS.md            the spike log: what was measured, what breaks, what it means
lean-run.png           screenshot of a verified run

There is no bundler and no tracked node_modules. The page loads the package's IIFE build — self.leanWasm.createCompiler({ baseUrl }), the same artifact a worker gets from importScripts — and that build is copied into public/vendor/ by a script rather than committed by hand, so there is still exactly one implementation of the driver.

public/ is deployable as it stands, which is the point of vendoring it. An earlier version imported the package's ES module entry through a /vendor/lean-wasm/ path prefix that only serve.js knew about: correct locally, and on Cloudflare Pages the request fell through to the SPA fallback, came back as index.html, and the browser refused to run it as a module — Expected a JavaScript-or-Module script but the server responded with a MIME type of "text/html". A static host serves files, not routes; serve.js is now deliberately as dumb as the host it stands in for, so this class of mistake fails locally too.

Verifying

what	command
mirror the artifacts	npm run assets
serve the page	npm start → http://localhost:8129/
serve the canonical single-threaded mirror	npm run start:canonical
see the isolation failure	npm run start:no-isolation
re-vendor the package build	npm run sync:vendor
syntax-check and drift-check	npm run check
verify a mirror against mirror.json	npm run verify:mirror -- <dir>
run the browser suite against a mirror	npm run test:browser

The page exposes document.documentElement.dataset (status, stage, runs, isolated, exitCode, initMs, runMs) and its element ids as globals, so a headless probe can drive it without string literals. window.__raw holds the last run's unclassified stdout/stderr.

The only other query parameter is ?syntaxCheck=, which controls the syntax check described under Limitations: auto (default), full, or 0.

Packaging and hosting

The page is code, not assets: public/ is ~30 KB, and everything else is mirrored and gitignored. So a package can ship the code and let the assets come from a CDN. All assets live in three sibling directories under one base:

<base>/lean-wasm/     binaries (lean.js, lean.wasm) + the packed core layer    96.4 MiB
<base>/lean-lib/      per-file libraries (Std, Lean, Batteries)                377 MiB
<base>/lean-mathlib/  the packed Mathlib layer                                 316 MiB

The canonical single-threaded mirror (wasm-build/out/mirror-upstream) adds compressed layouts under lean-wasm/: lean.js.gz (2.2 MB from 45.8 MB, 20×), lean.wasm.gz (16.7 MB from 97.5 MB, 5.8×) and snapshots/*.snap.gz (372 MB for the four, from 902 MB raw). The runtime probes all of them first and falls back to the plain files, so a host may ship either.

The directory is one deployable unit described by mirror.json (schema 1): the artifact/core/Mathlib commits and versions, and a sha256 of every pack, snapshot, glue file and manifest, under an id such as lean-62b6a2291302-dfe495316874-d53cc995. Check a deployed copy with npm run verify:mirror -- <dir>; a commit difference between the artifact and the assets is reported as a note, not a failure.

That is exactly the layout of public/, so the default (npm start) is the same origin's root, and a single ?baseUrl= moves all three at once:

http://localhost:8129/?baseUrl=https://cdn.example.com/lean

The host must send two headers, and they are not interchangeable:

header	needed for
Access-Control-Allow-Origin	everything fetched with fetch() — the binaries, core packs and layer packs
Cross-Origin-Resource-Policy: cross-origin	lean.js, which the worker pulls in with importScripts() — a no-cors request that COEP checks against CORP rather than CORS

Miss the second and every asset downloads fine but the boot dies with Failed to execute 'importScripts' … failed to load, which reads like a network problem and is not one. serve.js sends both, so a CDN layout can be tested locally: run npm start, start a second instance on another port, and point ?baseUrl= at it (http://localhost:8131 in development).

The page's own host needs two more, and they are not optional either. Isolation is what makes SharedArrayBuffer exist, so a site serving the page must send Cross-Origin-Opener-Policy: same-origin and Cross-Origin-Embedder-Policy: require-corp — the package cannot arrange this for itself. Cloudflare Pages reads those from a _headers file in the published directory, which is what public/_headers is, so the directory uploads as it stands:

npm run sync:vendor     # refresh the vendored package build (committed, drift-checked)
# upload public/        # the page, _headers, vendor/, and the three asset directories

One directory then serves both the page and the assets, which makes the deploy its own baseUrl — and the isolation the page needs is also what a LiveCodes embed would need from the same origin.

Upstream's library data is already CORS-enabled (Access-Control-Allow-Origin: *), so the 347 MiB of packs and .olean files could be fetched from lean.cau.li with no hosting. The two binaries are not — they are served through a Cloudflare Function with Cross-Origin-Resource-Policy: same-origin and no CORS — and they are the only part that must be hosted deliberately.

lean.wasm is 96.2 MiB, which rules out the obvious free CDNs:

• jsDelivr has a 20 MB per-file limit on top of the 150 MB package limit, so the wasm cannot be served there at all (the 5 core packs, ~6 MB each, would fit).
• GitHub Releases send no Access-Control-Allow-Origin (and Content-Disposition: attachment).
• GitHub Pages does send * and would hold the file under its 100 MiB limit, but is not intended as a CDN and has a soft 100 GB/month bandwidth cap.

Cloudflare R2 / B2 / Bunny (96 MB stored is cents per month; egress free on R2) — or asking upstream to add the header — is the way to host the binaries. Full audit, including the HEAD-vs-GET trap that makes this look the opposite of what it is, in FINDINGS.md §5.

Status

Spike complete, and the isolation problem is solved rather than worked around. wasm-build/ builds a single-threaded Lean wasm whose memory is unshared, and this page runs a proof on it in a document with no cross-origin isolation and no SharedArrayBuffer — crossOriginIsolated: false, exitCode 0, boot in 3.4 s (FINDINGS.md §9.7). The page serves either artifact without configuration, because the runtime reads the requirement off the wasm before it boots.

The canonical mirror (wasm-build/out/mirror-upstream) now ships four host-baked snapshots, gzipped, and the first-run numbers on a non-isolated page are: Init 0.37 s, Std 6.0 s, Lean 9.8 s, Mathlib 184.7 s (all exit 0; without the snapshots Lean is 137 s and Mathlib 605 s — FINDINGS.md §9.15). The last two are the important change: Lean and Mathlib were un-snapshottable, but only when baked against the artifact's own build tree; against the served tree all four save. The 54-second first compile is gone.

What is left is deployment rather than a wall: publishing the mirror (~1.0 GiB static, of which 372 MB is the gzipped snapshots), versioning artifact + layers + snapshots as one unit, and exercising Safari and mobile (Chrome is measured and Firefox works; neither of the other two has been tried).

License

MIT © Hatem Hosny. The Lean compiler and its libraries are Apache-2.0 (Lean project); the WASM artifacts and the worker's structure come from cauli/lean4-wasm-in-browser (Apache-2.0). See LICENSE.