Web-based prover UI

Stream: general

[Sebastian Reichelt]

Hi! I hope it's OK for me to post this here. I'm building a web-based interactive theorem prover at https://sreichelt.github.io/slate, with a rendering infrastructure to improve readability. The basic idea is that every definition in the library also includes a specification that describes how to render it. Seeing the Lean+LaTeX discussion above, I wonder if someone would be interested in combining this with Lean.

Eventually, the goal is that users can directly edit the rendered content online without having to look at the source code at all, but the web-based version only includes a minimal proof of concept at the moment. (It works in a desktop-based predecessor, but I never managed to finish it.) But for a start, read-only rendering of Lean source code already seems useful.