Lean implementation in Javascript?

Stream: general

[Nilesh]

Hello all,

I'm a working programmer and a student of mathematics. I am planning to build a visual proof-assistant on an infinite canvas where lemmas becomes nodes of a graph and tactics/proofs become the edges. It's going to be challenging but at least I will end up learning a lot on the way.

Because this will be web-based, I was wondering if someone has managed to implement Lean in browser-compatible Javascript. I am not very knowledgeable in C/C++, so I'd prefer a clean-room pure JS implementation, rather than those transpiled using Emscripten or WebAssembly.

If a Javascript implementation of Lean isn't available, I'd be interested in writing one. Are there any resources to help a programmer implement a Lean-like language from scratch? My aim is to retain full compatibility so that entire mathlib could be imported as-is.

[Eric Wieser]

Are you aware of https://leanprover-community.github.io/lean-web-editor?

[Eric Wieser]

That already runs Lean in the browser, I believe using Emscripten WebAssembly

[Eric Wieser]

If a Javascript implementation of Lean isn't available, I'd be interested in writing one. Are there any resources to help a programmer implement a Lean-like language from scratch?

You might also be interested in Joachim Breitner's http://incredible.pm, which has an interactive canvas for proving very basic results

[Nilesh]

@Eric Wieser Yes, I had seen the Web editor. The Webassembly version could be the last resort. My intention is to explore more visual than textual proofs (kinda like circuit simulators). The second link is highly relevant and had a link to this paper. Thanks for sharing that.

I am willing to start from scratch and learn. So even tutorials on implementing Dependent Type Theory would be quite helpful. :)

[Eric Wieser]

Reimplementing Lean 3 from scratch in a way that lets you interface with mathlib sounds like a rather hard and pointless project. I think you should decide whether you care more about building something from scratch (in which case I don't think it should aspire to be a copy of lean), or about exploring the data in mathlib (in which case you can just use lean!)

[Jason Rute]

If you are not committed to a browser interface but instead just committed to a visual interface, you should look into @Edward Ayers widgets which are a visual interface to Lean which run in vs code. The goal view of lean with its interactive features are implemented in widgets. Moreover, people have made various other visual tools with widgets. If you search here on Zulip you should be able to find some.

[Eric Wieser]

Another direciton you could go is to parse the raw low-level output of lean, such as what https://github.com/gebner/trepplein does. If I understand correctly, the low-level output still contains enough information to draw the type of graphs you're thinking of

[Nilesh]

I think @Joachim Breitner 's http://incredible.pm already does a lot of what I wanted to build. Instead of building something from scratch, I will now play with its source and see what it would take to extend its capabilities to be able to prove theorems about natural numbers or abstract algebraic structures. It currently goes till Simply typed Lambda Calculus which is quite a lot. There is even an Isabelle proof that their port graph approach is as powerful as natural deduction.