"Quantity has a quality all its own" Also, and perhaps easier to wrap one's head around, is issues of tooling. Already, there is a very heavy use of "tactics"

"Quantity has a quality all its own" Also, and perhaps easier to wrap one's head around, is issues of tooling. Already, there is a very heavy use of "tactics" (metaprograms, and ones with decent computational complexity (think "search" not just "expansion")). Mathematicians write lemmas so we can try to run the tactics on "mini problems" that do not grow even as the total body of work grows, but there's always a risk the that there's some sticking point one cannot break down enough.