Not sure how true this restrictions is once you have the agents hammering on at a big code base of formalised proofs.

Proofs stretching thousands of pages are split into lemmas, grouped into sub theories.

What I haven’t seen agents do yet is to develop new ideas for entire such theories. I have usually seen them bite into some existing idea and grinding out related results. But I am less sure than ever that they won’t!