I haven't tried it, but I saw Leanstral, an LLM specialized in writing Lean proofs, posted on HN recently and it claims to outperform some larger general purpose models. It didn't beat Claude Opus, but it seems to do decently at one tenth the cost. It's plausible that further research could yield other models that are smaller and more effective at limited tasks, reversing the trend of ever growing models.