Proof Assistants Stack Exchange is a question and answer site for mathematicians and computer scientists who develop and use proof assistants. It only takes a minute to sign up.
Sign up to join this community
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.
Here is what I think is going on, but I could be (possibly very) mistaken on the details.
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.
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).
