I'm looking at the Lean-in-the-web-browser setup here. It would be really cool if my server at linearlibrary.net could have a page for Lean code of its own.

Unfortunately when I tried to take apart the code here it doesn't work anymore. I tried downloading the constituents of the webpage but it makes for a frozen page. I was wondering if anyone can direct me to how I could set up this web-Lean on a site of my own.

  • $\begingroup$ Your question title and content don't align. You ask about Lean 4, but post a link to a Lean 3 web editor. The lean community could do a much better job at distinguishing the two versions, so you might just be mistaken on the difference. My answer below covers both versions. $\endgroup$
    – Jason Rute
    Jan 29, 2023 at 18:51

1 Answer 1


Here is what I think is going on, but I could be (possibly very) mistaken on the details.

Lean 3

Lean 3 has the ability to run in JS/WASM, so the Lean 3 web editor (which is what you linked to above) is actually running Lean in your browser if I'm not mistaken (GitHub source). The Lean 3 Natural Number Game runs the same way, using the Lean Game Maker.

Lean 4

I don't think Lean 4 has this ability (currently) to run in JS/WASM. So instead, one has to run it on a server and have an editor in the browser which communicates with the server as in the Lean 4 web editor (GitHub source and Zulip discussion). Similarly, see the Lean 4 natural number game, its GitHub source, the Lean 4 Game Server, and discussion on Zulip (which I think are all early works in progress).

In general, if you are interested in hosting something similar yourself, I would post more about it on the Zulip chat, solicit advice, and be prepared to get your hands dirty with lots of technology, since this is all very bleeding edge (especially Lean 4).


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.