> 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 flo

> 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.