Inference providers no longer hosting Lean 4 models

Stream: Machine Learning for Theorem Proving

[(deleted)]

Right now, both Novita and DeepInfra no longer host the DeepSeek-Prover-v2 model. The Kimina Prover demo website is no longer usable. While I can still make do by renting a GPU at around $2/h, it's expensive. Are there other options? Can anyone set up a service for a Lean 4 model? If resources are limited we could focus on hosting the most powerful model, Goedel Prover v2.

[(deleted)]

Update: the Kimina Prover demo website is now usable.

[(deleted)]

But I need to use a VPN. Looks like Viettel's terrible routing strikes again.

[(deleted)]

I recommend that you use RunPod or vast.ai. Very cheap.

[Eric Rodriguez]

I would recommend using Aristotle through the app :)

[Jason Rute]

That kind of sounds like a clunky interface. If you have an iPhone and a Mac, I guess it isn’t that hard to paste back and forth, but still.

[Eric Rodriguez]

Yeah, it is a bit unfortunate on that front :(

[Ralph Furman]

Where is Aristotle? I haven’t been able to find it on the App Store nor on the harmonic website

[(deleted)]

Gated behind a waitlist. And might not even exist.

[Eric Rodriguez]

I can confirm it certainly exists; for waitlist -> https://aristotle.harmonic.fun