Integrating Lean with Godot for a browser game

Stream: general

[Victor Liu]

Hi everyone,

I'm working on a project where I want to integrate Lean with a Godot-based math game that will be deployed as a static page on GitHub Pages. Based on search results, it seems like I have to compile Lean to WebAssembly (WASM) so it can run in the browser and interact with the game.

Are there resources that can help me get started with this task? Something like a tutorial would be very helpful because I am new to this, being only familiar with Godot and JavaScript, but not working between different languages in the same application.

Thanks in advance for any help!

[Utensil Song]

You may get started by trying out lean2wasm, but in general using Lean in a browser only game is still a dream in the long run. At the present stage you might want to also evaluate the lean4web approach, i.e. you need a backend server to run Lean in "containers" (not docker).

[Utensil Song]

What kind of games are you planning to make?

[Victor Liu]

For now probably just procedural operations like taking derivatives and integrals, and I would like to extend it later which is why I am looking into Lean

[Victor Liu]

Ideally I want the application to be client-side and self-contained to avoid additional headache

[llllvvuu]

would the gamer be provide proofs for these derivatives/integrals? if you're trying to calculate derivatives/integrals, there aren't tactics for that (yet), though you can do that in JavaScript with some symbolic maths or autodiff library

[Utensil Song]

For interactive math games, you might also have better luck with ProofWidgets.

[Jon Eugster]

For compiling to WASM, maybe @Alexander Bentkamp can give you more details (once back from holidays). He did the heavy lifting behind lean2wasm linked above..

I dont know enough about godot, but you might be able to set up a game at adam.math.hhu.de (which isnt published on the front page) and then integrate this directly inside your app (which would require internet access, but at least you're not bound to serting up your own lean server...). And if you describe in more details how you would like to embed this project (or parts of it) into yours at https://github.com/leanprover-community/lean4game there might be a small chance that it'll be done.

I've also had it on my mind to clean up lean4web to make it easier to import just the editor in any other project, so again if you have a very specific usecase, having a github issue describing it would be helpful

[Arthur Paulino]

[I read the title too fast and I thought you wanted to enable Lean 4 programming to create games in Godot, which is something I wanted to do a few months ago :smiley:]

[Max Nowak 🐉]

(Lean4 game engine when)

[Victor Liu]

Thanks to everyone for the advice. I'm thinking of making the front-end UI with Godot as it is more suited for making great game visuals and logic, whereas I could keep Lean in the backend logic for handling the actual mathematics. In this light, I am not sure if ProofWidgets is appropriate for this goal, as it appears to be its own UI library?

[Victor Liu]

I have found the following resource on GitHub: lean-client-js, a "JavaScript library to interface with the server mode of the Lean theorem prover". However, it appears that it was made 7 years ago and is for the Lean 3 version. Is it possible to make this work for Lean 4?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I don't think that exists as a standalone library for Lean 4. Your best bet would be looking at the source code of lean4web and perhaps Paperproof which also contains its own, standalone connection to the Lean server.

[Victor Liu]

Is the Lean server an external online-hosted one? Or can you host it client-side? I'm a bit confused by the terminology, sorry.

[Victor Liu]

My goal is to minimize external dependencies, and make it as standalone as possible

[Victor Liu]

I'll probably look for symbolic languages in JavaScript for now, I think it will be quite a lot simpler. Thanks a lot for the help!

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Victor Liu said:

Is the Lean server an external online-hosted one? Or can you host it client-side? I'm a bit confused by the terminology, sorry.

It is a language server in the sense of LSP. It usually runs on the same machine as the editor, but as a separate process. It can also run on a different machine when using a remote setup such as via the VSCode SSH extension.