In-Browser Lean 4

Stream: mathlib4

[Dean Young]

Hi, All,

I have a server of Linear Library and I want to install an edit page which can edit and compile Lean 4. Is it possible to use existing code for this?

[Jon Eugster]

Probably not exactly what you're looking for, but there is lean.math.hhu.de which runs lean4 online and the code for that is on github (github.com/leanprover-community/lean4web).

[Eric Wieser]

From the readme (emphasis mine)

in this web editor, the Lean server is running on a web server, and not in the browser

[Jon Eugster]

That is correct

[Dean Young]

Thanks for your help guys!