basic server/API library

Stream: Is there code for X?

[Avi Craimer]

Are existing frameworks for using Lean as a Backend. I'm thinking about building a web app that is able to interact with Lean.

There is the game server: https://github.com/leanprover-community/lean4game/tree/main/server/GameServer

I'm just wondering if this is the best starting point, or if there is a more basic server library.

Also if anyone knows of any tutorials for using Lean as a backend that would be super helpful.

[Jon Eugster]

I think the official documentation is this Lean/Server/README.md.

In it's current shape I don't really recommend looking at GameServer as a first entry point :grimacing: but I hoped to clean that up over the next month...

[Avi Craimer]

Thanks @Jon Eugster

Does the Lean server extension offer a way to emit JSON about tactics state, type errors, etc, to another process such as a Node.js service?

I'm thinking this would be useful when running in VSCode to have real time message passing to another service, for example, one which could easily interface with LLM APIs.

[Kim Morrison]

https://github.com/leanprover-community/repl

[Avi Craimer]

Kim Morrison said:

https://github.com/leanprover-community/repl

Thanks that looks like exactly what I need!

[Kim Morrison]

(It's meant to be undergoing a major revision at the moment, but other priorities have been getting in the way for the last two months...)

[Mr Proof]

Have you seen this: https://github.com/openai/lean-gym It's open AI's experiments with Lean.

[Kim Morrison]

Not sure who you are asking, but yes, "we" have seen this. :-) It is quite old by now and that exact direction isn't being pursued.

[Mr Proof]

:) Just pointing that out to Avi since he was talking about LLMs and such like.

[Jason Rute]

If you are interested in interfacing Lean with LLMs, be sure to check out #Machine Learning for Theorem Proving. There has been a lot of work since Lean-Gym in this area. (Although most experiments are done in a way where the system is not practical for Lean users to use.)