3 ms·
> 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
by nextaccountic 8d ago
> 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
- LiamPowell 8d agoThe 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.
- nextaccountic 7d agoNowadays 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