How to distill my own models?

I've been using cloud provided models for agentic theorem proving a lot, and cost is becoming an issue for me. I have funding for hardware cost but I can't use them for LLM credits which put me in a unique situation where it might be cheaper to self-host models instead of paying cloud models.

The problem is that theorem proving is a very niche use case that smaller models don't really understand, so I was thinking maybe I could distill this ability from a larger model and train my own reasonably sized model for theorem proving. Is this a good idea?

Edit: I'm aware DeepSeek has a fine tuned model for Lean but I'm doing Rocq and there's surprisingly little LLM models for Rocq. Maybe another possible route is to post-train the DeepSeek model on Rocq?