Run Lean 4 in the browser via WebAssembly.

_{This project is mainly based on @cauli's work to compile Lean 4 to WASM: cauli/lean4, with a web playground reference from cauli/lean4-wasm-in-browser.}

npm install lean4.js

import { Lean4 } from 'lean4.js'

const lean = new Lean4()
await lean.init()

const result = await lean.run('#eval 2 + 2')
console.log(result.stdout)   // "4"
console.log(result.exitCode) // 0

lean.dispose()

WASM assets are loaded from cloudflare R2 automatically. No extra setup needed.

Note: Your page must be served with COOP/COEP headers for SharedArrayBuffer support. See COOP/COEP setup below.

1. Reduced unnecessary .olean artifacts in lean-lib (for example, private artifacts such as olean.private), bringing the lean-lib size down to about 90+ MB and the full bundle to about 300+ MB. This is acceptable for now, and there is still room for further size optimization.
2. Published lean4.js to npm for easier integration and reuse.
3. Deployed a web playground so people can try it directly in the browser.

1. Even running a minimal Lean file still takes close to 1 minute, which is hard to use in production today.
2. We tried to support --server/--worker mode in the browser, but this attempt failed. If startup can be paid only once (instead of per run), the project would become much more practical.

Downloads and caches the .olean library bundle. Must be called before run(). Uses IndexedDB to cache for subsequent visits.

Runs Lean 4 code in an isolated iframe.

Returns { stdout: string, stderr: string, exitCode: number }.

Cleans up resources.

SharedArrayBuffer requires these server headers:

Cross-Origin-Opener-Policy: same-origin
Cross-Origin-Embedder-Policy: require-corp

import { lean4Plugin } from 'lean4.js/vite'

export default defineConfig({
  plugins: [lean4Plugin()],
})

Add headers in your server/hosting config (Nginx, Vercel, Netlify, etc.).

If you prefer not to use the CDN:

npx lean4-wasm-copy public/lean4-wasm

const lean = new Lean4({ basePath: '/lean4-wasm' })

MIT