> 1. Tokens are really expensive

Just don't use frontier models by American labs. Chinese models are much cheaper and competent enough for most stuff

> 2. The context window becomes flooded with proof work rather than work on the original problem,

This can be solved by doing proofs in subagents. You can even have a tree of agents, for demanding proofs. They can share a database or otherwise have communication channels if some of them stumble upon something relevant for another agent