Comment by octoberfranklin

Experience from other agent-based verification projects, such as MachCSL, suggests that the answer might be no: the agents hit a complexity wall with the verbose proof style, and scaling up requires the proofs to be structured around better modular abstractions and reasoning principles.

This is not just plausible but in fact the most likely result.

We already have plenty of evidence of this phenomenon in programming. LLMs are awesome for working on human-written or at least human-reviewed codebases.

But when you set them loose without a human around to force them to refactor their code into something that fits in meatbag-brain-sized contexts, they drift into the ghastly nightmare of the Anthropocene (go ahead, take a look at the leaked source code for Claude Code). They can handle this for a while, especially if you're doubling your model's weight count every four months.

But when you stop doing that, they choke on their own spaghetti.

It's like Feynman said about teaching -- great theoretical physicists need to re-explain the basics to students from time to time in order to force them to come up with not just the correct physical laws, but the simplest version of those laws. Take away that constraint -- IAS or LLM -- and eventually it all goes wrong.