Lean in the cloud as an API or pip package - options

Stream: Equational

[Michael Bucko]

What options do I have to run Lean in the cloud as an API? I know about Lean 4 Web, but I am not sure I can run it as an API.

Spoke to @Josh Clune and learnt that, if I run Duper as an executable, I'd lose the soundness guarantees (afforded by having Lean's kernel verify the proof Duper produces).

And that's critical that one can keeps the soundness while building or using an API.