Question: Why does lean4web not run in the browser, eg via WASM or similar?

Open samuela opened this issue 3 months ago • 2 comments

The README suggests that lean3web featured running in the browser and not requiring any backend support, but that lean4web does not support this. OOC why is this the case? Would having fully in-browser support be a welcome feature?

Oct 13 '25 16:10 samuela

You can read the history about attempts to build Lean in WASM here: https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/wasm.20build

but in short, even if compilation to WASM was featured, Lean4 and mathlib4 are just much bigger and it would be infeasible to provide them in a wasm build

Oct 14 '25 20:10 joneugster

Thanks @joneugster! Sad to hear that this is not yet feasible. Hopefully we can figure out how to get the download size smaller eventually.

Oct 15 '25 16:10 samuela