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.

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/ since embedding it here makes it pretty narrow.