> 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
The problem with using subagents is that you often have to rewrite a chunk of a program in a more proof-friendly way, just saying "go prove this code, don't edit it" doesn't work. Maybe I'm underestimating how effectively subagents can communicate though and they'd be fine asking for changes.
Nowadays agents know a lot of tricks on how to effectively prompt subagents
Generally speaking the ouput of a subagent is sent directly to the calling agent, that can make the final edits. Or, the subagent can edit the file in a local copy, and the calling agent can diff it