Lean in the Browser

Developer Kshitij Lakhina published a working WebAssembly build of Lean 4 and its language server, hosted at kshitijl/lean-wasm, with a browser demo at /demos/lean-wasm/demo/. Lakhina built it to support an in-progress interactive game that teaches Lean to programmers through specs and proofs for code rather than math. The demo does not work on phones; Chrome performs best, Firefox works but is slower, and Safari is unstable and slow.

Lean in the browser I hacked together a working wasm build of Lean 4 and its language server. For details on how it works see kshitijl/lean-wasm https://github.com/kshitijl/lean-wasm . I did it to make an interactive game that teaches Lean to programmers , so it’s focused on specs and proofs for code rather than math. That’s still work in progress as I figure out the material, levels and so forth. In the meantime, here’s a demo of Lean in the browser For now it doesn’t work on phones. Chrome is best, Firefox works but is slower, Safari is unstable and pretty slow. There’s also a full page demo at /demos/lean-wasm/demo/ https://klauria.tech/demos/lean-wasm/demo/index.html since embedding it here makes it pretty narrow.