QED64: Lean 4 in your browser, 64-bit

QED64 is a Lean 4 editor in the spirit of live.lean-lang.org, with one difference: no server checks your proofs. The real Lean 4 compiler and language server run in a Web Worker as WebAssembly Memory64 (64-bit pointers, shared memory, pthreads). Lean's core library and a 4,438-module Mathlib environment are loaded from verified, content-addressed environment snapshots. The page is lean4monaco (Monaco plus the vscode-lean4 InfoView) over that in-browser LSP. It serves Lean 4.35.0 and Mathlib v4.35.0 (docs/PROVENANCE.md).

Live: https://qed64.fawadworkaddress.workers.dev/

Requirements

To use it (a browser):

• Desktop Chrome/Edge 133+ or Firefox 134+: WebAssembly Memory64 and SharedArrayBuffer. Safari has no Memory64 and is out of scope.
• Cross-origin isolation. The top document must be served with Cross-Origin-Opener-Policy: same-origin and Cross-Origin-Embedder-Policy: require-corp, or Memory64 shared memory does not exist. The live site, npm run dev and npm run preview:prod all send these headers.
• Memory. A tab takes about 2.5 GB once the Mathlib environment is loaded (measured 2026-11-02 on runtime wasm64-36d7f415, docs/HARDENING.md #55). Only one QED64 runs per top-level page. On an 8 GB machine, close other heavy tabs first.
• Browser storage. About 1.5 GB free in the browser profile (OPFS) for the Mathlib environment's cached region.

To build or test it:

• macOS or Linux, Node 24+ (Memory64 on by default) and npm.
• Disk: npm run fetch:artifacts writes about 1.6 GB into public/ (the runtime, 106 MB; the two profile packs, 1.14 GB; the two snapshots, 351 MB). Adopting a release and rebaking needs 12 GB free under work/ (16 GB with --fat-tree), the floor pipeline/release/adopt-release.sh checks.

Which Mathlib

The page serves a curated part of Mathlib v4.35.0: 2,432 of its 8,624 modules, chosen for download size and memory (with Lean, Std, Batteries, Aesop and the other dependencies they make the 4,438 modules above). import Mathlib and import Mathlib.Tactic load exactly that part, so a name from an area it leaves out is "Unknown identifier" here although native Lean knows it. It has none of CategoryTheory, Probability, FieldTheory, AlgebraicGeometry, AlgebraicTopology, ModelTheory or RepresentationTheory, and almost none of MeasureTheory, NumberTheory or Combinatorics. A module outside the part, imported by name, is refused with a note on the import line. While such an error stands under import Mathlib, the page shows "not all of Mathlib is here" beside the status pill; its version tooltip names the Mathlib commit.

The browser's stack

A browser gives Lean far less stack than desktop Lean has, so a very long file, a very long proof or a very deep decide can run out of it. Lean then reports an error ("… the WebAssembly runtime's stack is exhausted …") on a command it could not check. The error stays, because that command is not verified, but the page adds a note to it saying that this is a limit of running Lean in a browser rather than a mistake found in the proof, and what helps; the status pill then reads "ready — N places not checked (browser stack limit)". When the recursion gets past Lean's own check, the page pauses checking until the next edit.

Use QED64

There are three ways, from least to most code. The contract for all three is docs/EMBEDDING.md (v1). §6.1 there is a complete, tested recipe.

(a) QED64's page in an iframe

Build the shell from a QED64 checkout at the commit you pin (see "Build from source"). Serve dist/ at your origin root, with /runtime/, /profiles/ and /snapshots/ beside it. Then frame /?embed=1:

<!-- your page, on the same origin as QED64's dist/, sent with COOP same-origin + COEP require-corp -->
<script type="module">
  addEventListener("qed64:frame-api", async ({ detail: { api } }) => {
    api.on("diagnostics", (d) => console.log(d.version, d.diagnostics));
    await api.setDocument("import Mathlib\n\nexample : 2 + 2 = 4 := by norm_num\n");
    console.log((await api.settled()).phase);   // "ready"
  });
</script>
<iframe src="/?embed=1" allow="clipboard-read; clipboard-write" style="width:100%;height:80vh;border:0"></iframe>

• Same origin only in v1. The frame inherits cross-origin isolation from your page, so your page needs the COOP/COEP headers too. A cross-origin frame cannot boot, so you cannot frame the live site from another origin.
• Embed mode (?embed=1) hides the examples menu and the page's own controls (Open…, Download, Copy link, Show the editor while Lean loads, the curated-Mathlib note, the splitter) and leaves persistence to you: listen for the document event and call setDocument.
• Look. The plain page follows the OS light or dark scheme, also when it changes; a ?embed=1 frame stays light. In a window or frame 720 px wide or less, it puts the InfoView below the editor. On the plain page, drag the gutter between the editor and the InfoView to resize them.
• Files. On the plain page, Open… (Ctrl/Cmd+O) opens a .lean file of up to 2 MiB as one undoable edit, and Download (Ctrl/Cmd+S) saves the editor's text as a .lean file.
• Editor. Shift+F12 lists a name's uses in the file, and F2 renames them once the status reads ready. Lean answers both only for a whole project, so the page computes them for its one document. A space after a function or theorem shows its parameters (Ctrl/Cmd+Shift+Space shows them again), and the InfoView's trace messages have a search.
• URL parameters (docs/EMBEDDING.md §3–§4): #code=<text> and #codez=<LZ-string> (lean4web's spellings: a boot document only in a same-origin frame; on the plain page the fragment is a share link that opens behind a consent gate, docs/HARDENING.md #77, and the bar's Copy link writes one for the editor's text), snapshots=<dir> (an overlay set on this origin), profiles=<dir> (validated, then ignored since 2026-11: no library pack is read), runtime=<buildId>, memory=<GiB> and edithold=<n>. A refused value fails the boot and names the parameter.
• The page API is globalThis.qed64.api (§2): setDocument, settled, status, restart, and the boot, ready, diagnostics, document, death and reboot events. Feature-detect with api.capabilities.

(b) qed64/embed in your own page

Install QED64 as a git dependency pinned by a full commit (npm honours its files; there is no npm registry release):

{ "dependencies": { "qed64": "github:FawadHa1der/QED64#<40-hex commit>" } }

You need four things (docs/EMBEDDING.md §6.1). First, COOP/COEP on your page, and in Vite optimizeDeps: { exclude: ["qed64"] } and build: { target: "es2022" } (the code below uses top-level await, which Vite's default target refuses). Second, the six workers that embedding/closure.json lists, copied to their serveAs paths before every build. Third, the artifacts at /runtime/, /profiles/ and /snapshots/ on your origin: the package does not ship the tracked manifests, so fetch QED64's served set with them from a QED64 checkout at your pin, node node_modules/qed64/pipeline/release/fetch-artifacts.mjs --manifests <QED64 checkout>/public --out public --with-manifests (EMBEDDING §6, §6.1 step 4; without --manifests it refuses). Fourth, the code below. The workers step is a short prebuild script:

// scripts/stage-qed64-workers.mjs: run before every dev start and build
import fs from "node:fs"; import path from "node:path"; import { createRequire } from "node:module";
const pkg = path.dirname(createRequire(import.meta.url).resolve("qed64/package.json"));
const closure = JSON.parse(fs.readFileSync(path.join(pkg, "embedding/closure.json"), "utf8"));
fs.rmSync("public/workers", { recursive: true, force: true });
for (const { path: from, serveAs } of closure.workers) {
  fs.mkdirSync(path.dirname(`public${serveAs}`), { recursive: true });
  fs.copyFileSync(path.join(pkg, from), `public${serveAs}`);
}

Without the editor, your code is the language client. It boots a session behind the relay and speaks JSON-RPC on one MessagePort. This is docs/EMBEDDING.md §6.1 (a) verbatim (npm run test:consumer checks that the two copies match, then type-checks and builds it). It uses top-level await, hence the build.target above. The pagehide line is required: without it every reload leaves a dead multi-GiB Memory64 heap behind until the renderer is killed (EMBEDDING §7.9, unload()):

import { LspRelay, MEMORY64_PROBE, ResidentSession, installArtifacts, makeEditorPolicy, type StatusSink } from "qed64/embed";

if (!crossOriginIsolated || !WebAssembly.validate(MEMORY64_PROBE)) throw new Error("needs COOP/COEP and Memory64");
const ui: StatusSink = {   // progress as data (§7.1)
  busy: (label, info) => console.log("busy", label, info?.stage),
  progress: (label, info) => console.log(label, info?.loaded, info?.total),
  idle: (label) => console.log("idle", label),
};
const artifacts = await installArtifacts(ui, { overrides: "none" });   // manifest, snapshot index
const policy = makeEditorPolicy(artifacts.snapshots);                    // snapshots and memory per header
let current = "import Mathlib\n\nexample : 2 + 2 = 4 := by norm_num\n";   // what a (re)boot serves
const relay = new LspRelay(
  (opts) => new ResidentSession({ artifacts, ui, policy, headerText: current }, opts ?? {}),
  { status: (s) => console.log(s.relay, s.phase, s.lastDeath?.cause?.kind ?? "") },   // deaths, §7.2
  () => new Promise((r) => setTimeout(r, 1500)),
);
addEventListener("pagehide", () => relay.unload(), { once: true });

const port = relay.clientPort, uri = "file:///project/Probe.lean";
port.onmessage = (e) => { if (e.data.method === "textDocument/publishDiagnostics") console.log(e.data.params.diagnostics); };
port.postMessage({ jsonrpc: "2.0", id: 0, method: "initialize", params: { processId: null, rootUri: null, capabilities: {} } });
port.postMessage({ jsonrpc: "2.0", method: "initialized", params: {} });
port.postMessage({ jsonrpc: "2.0", method: "textDocument/didOpen", params: { textDocument: { uri, languageId: "lean4", version: 1, text: current } } });
// an edit: update `current`, then a full-text didChange (coalesced, §7.8)

With the editor, boot the same way (the pagehide line included) and hand relay.clientPort to lean4monaco instead of posting on it yourself, as QED64's own page does (frontend/src/main.ts):

await leanMonaco.start({
  websocket: { $type: "WorkerDirect", worker: { postMessage() {} }, messagePort: relay.clientPort } as unknown as { url: string },
});

The InfoView's static files are lean4monaco's to serve: copy @leanprover/infoview/dist/* and lean4monaco/dist/webview/webview.js to /infoview/ on your origin, as frontend/vite.config.ts does, or the InfoView frame 404s (QED64's copy also patches webview.js so widget panels get their RPC right, docs/HARDENING.md #56).

The library API (progress, failure causes, deaths, overlays, edit coalescing) is docs/EMBEDDING.md §7. npm run test:consumer builds a consumer from the packed tarball (tests/consumer/fixture/ plus the block above).

(c) qed64/edge in your own Cloudflare Worker

qed64/edge is the edge-worker library that serves QED64 itself. It is one dependency-free ES module that sets the isolation headers, the cache rule, HEAD and Range on the artifacts, and the R2 key mapping:

// your Worker's main module (wrangler.toml: [assets] binding "ASSETS" with run_worker_first = true,
// [[r2_buckets]] binding "ARTIFACTS")
import { createWorker } from "qed64/edge";

export default createWorker({
  r2Prefix: (env) => env.R2_PREFIX,               // e.g. "my-site/" in a shared bucket; unset: the bucket root
  rootRedirect: (env) => env.ROOT_REDIRECT ?? null,
});

docs/DEPLOY.md "Using qed64/edge in your own Worker" has the full wrangler.toml, every option, the release option that reads the toolchain's files from a shared lean4-wasm64/<id>/ prefix, and the five ways it differs from a hand-written worker.

Build from source

git clone https://github.com/FawadHa1der/QED64 && cd QED64
npm ci                     # the root: library, pipeline, tests (and the pinned lean4-wasm64 package)
npm --prefix frontend ci   # the page: lean4monaco, Vite
npm run fetch:artifacts    # public/: runtime chunks, profile packs, snapshots (~1.65 GB), each sha256-verified
npm run build:site         # dist/: the page and the two indexes it deploys with (writes dist/qed64-build.json last)
npm run preview:prod       # http://localhost:5185, served by the live Worker's own code (infra/worker.js)

npm run dev is the Vite dev server instead (http://localhost:5184, COOP/COEP set). The tracked manifests (public/runtime/runtime-manifest.json, public/profiles/*.json, public/snapshots/index.json) pin every served byte by SHA-256. The bytes are not in git. fetch:artifacts downloads exactly what the manifests name (from the live site by default; --origin <url> names another deployment, --release <dir|url> a toolchain release), checks each file before it is renamed into place, and skips files already present (docs/CLI-CONTRACT.md "fetch-artifacts").

Where the compiler comes from. Nothing is compiled here. The wasm64 Lean toolchain (the patched compiler, its patch series, the runtime build and the library packs) belongs to the Lean fork FawadHa1der/lean4, branch qed64-wasm64, wasm64-build/. QED64 consumes its releases. The release it serves is pinned in toolchain/lean4-wasm64-release.json (schema lean4-wasm64.release/v1). The fork's lean4-wasm64 package is a devDependency, pinned by that release's tgz URL. The base trees the snapshots were baked from are recorded in embedding/base-tree.json. To rebuild the runtime itself, follow docs/REBUILD.md §1 in the fork. docs/PROVENANCE.md is the digest chain and how to verify it.

Adopting a new release. pipeline/release/adopt-release.sh --id <id> --digest sha256:<hex> --from <release URL> --public <isolated tree> … does the whole adoption: fetch and verify, base trees, both snapshot bakes, staging, an isolated promote, and base-tree.json. --dry-run prints the plan and writes nothing (docs/REBUILD.md §3).

Baking your own snapshots. A snapshot is binary-paired: bake it with the exact runtime you serve. The bake reads a runtime directory (bin/lean.wasm) and an olean tree. Fetch the runtime from the pinned release (id and digest in toolchain/lean4-wasm64-release.json) with the fork's CLI, as adopt-release.sh does for its $W/artifact, then bake into a directory of your own:

node node_modules/lean4-wasm64/cli.mjs fetch --from https://github.com/FawadHa1der/lean4/releases/download/<id>/ \
  --out <work>/artifact --only runtime --id <id> --digest sha256:<hex>
npm run bake:snapshot -- --name <name> --artifact <work>/artifact --lib <olean tree> \
  --work <work>/snap --out <work>/overlay --roots <A,B> --probe '<lean source>'

For an extra environment, serve that set as an overlay, with no promote: the page boots the base init plus at most one other entry (docs/EMBEDDING.md §8), so bake init into the same --out as well (REBUILD §3 step 8 has its command line), copy the directory to public/snapshots/<overlay>/ (bake-snapshot refuses an --out inside public/) and open /?snapshots=snapshots/<overlay>. To replace the served pair itself, use adopt-release.sh above: it stages the runtime and both snapshots together. npm run promote:staging takes only such a complete staging (runtime/runtime-manifest.json and chunks/, and every snapshot of the pairing) and replaces the served index wholesale. Every pipeline tool, with its flags, exit codes and stable output lines, is in docs/CLI-CONTRACT.md. The snapshot index's writer rules are docs/SNAPSHOT-INDEX.md.

Deploying (Cloudflare Workers static assets plus R2, one origin) is docs/DEPLOY.md. scripts/deploy-app.sh is the one deploy path.

Test

Three gates (docs/TESTING.md has every lane, its command, its prerequisites and its pass line):

• G0, needs no artifacts and no browser:

  npx tsc --noEmit && npm test && npm run -s typecheck:site && npm run -s build:site && node pipeline/snapshot/cli.mjs --check-preludes && npm pack --dry-run --json > /dev/null

• G1, end to end in a real browser, against the fetched artifacts (npx playwright install chromium first): npm run test:adversarial (preflight, then the compiler battery, then e2e 29/29; -- --skip-compiler on a fresh clone, because the battery needs Node-side build outputs). Add the page lanes tests/adversarial/{page-api,infoview-actions,liveness-faults,reload-storm,edit-storm,…}.mjs and the integration tier npm run test:integration (the real runtime under Node; QED64_LEAN_ARTIFACT names it). Run one browser lane at a time. On a machine shared with other sessions, run each through the host's browser lock.
• G2, the consumer view: npm run test:consumer -- --work <dir outside the repo> packs QED64, resolves every exports key from the extracted tarball, and builds tests/consumer/fixture/ (a qed64/embed page and a qed64/edge Worker) with the repo's tsc and Vite.

Layout

Path	What lives there
lib/	the library, qed64/embed (index.ts is the barrel): worker client, snapshot index, boot, session adapter, LSP relay, edit coalescer, causes, parameters
frontend/	the page (its own package.json): lean4monaco over the in-browser LSP, the page API, import completion, single-document references and rename
public/workers/	the six worker scripts (lean.worker.js runs the runtime; the LSP front door, framer, Memory64 probe, worker constants, snapshot prefetch)
public/{runtime,profiles,snapshots}/	the served artifacts: manifests tracked, bytes fetched (npm run fetch:artifacts), never committed
infra/	edge-worker.js (qed64/edge) and worker.js, the live site's Worker
pipeline/	snapshot/ (bake, probes, Node runner, the CLI contract), release/ (fetch, adopt, promote, verify, release manifest), artifacts/ (pack, olean reader, umbrella), toolchain/ (the path rule and the runtime buildId)
scripts/	deploy-app.sh (and its guard, deploy-guard.mjs), serve-dist.mjs (npm run preview:prod), upload-artifacts.sh
tests/	unit/, integration/, adversarial/ (the browser lanes), consumer/ (G2), mutation/
toolchain/, embedding/	the pinned toolchain release record; closure.json (what an embedder needs), base-tree.json and the served umbrella olean it names under umbrella/ (its off-host copy; not shipped in the package)
docs/	the contracts and the design record; docs/history/ holds superseded documents

License

MIT, see LICENSE. Lean, Mathlib and Batteries are Apache-2.0. The wasm build derives from cauli/lean4 reinstate-wasm (Apache-2.0).