Serverless Pantograph on Morph Cloud

Stream: Machine Learning for Theorem Proving

[Jesse Michael Han]

Hey guys, we just published an open-source template for running Pantograph servers with a REST API wrapper on Morph Cloud:

https://github.com/morph-labs/morphcloud-examples-public/tree/main/lean-server
https://morph.so/blog/lean-server-morph-cloud

Using Infinibranch snapshots it's easy to replicate and autoscale a running Pantograph server. This lets you do things like burst scale tactic executions for rollouts from a single environment + goal context to thousands of concurrent requests.

This is more elastic and can be more cost efficient than running a single Pantograph or Kimina server on dedicated large VM.