> Tokens are really expensive when we have a LLM

Expensive compared to what? Vs. human writing proofs they're definitely not.

> The context window becomes flooded with proof work

Context management is more art than science, but proofs are unusually good at compactation. Once proved, you can just keep the lemmas, you know,like humans do.