Finding common subexpressions in such a proof could be a separate field of research. It probably isn't a matter of looking for repeated strings.
I have some expertise in this field. My PhD is in combinatorics, which is closely related, and one of the main results used computer search. More, it's closely related to the Four Colour Theorem.
To me, what you say makes no sense at all. Perhaps this is what the field needs - people who know absolutely nothing making suggestions that are so far outside the box that those who have spent decades studying it would never consider them.
On the other hand, maybe there's nothing in it. Have you thought it through more? Do you have more ideas? Do you have any actual concept of what "sub-expressions" might mean in this context? Having written compilers for food I feel that I have some knowledge of the concept, but in this case it seems not to mean anything.
The way I read it, he was suggesting a possible way of reducing the size of the DRUP certificate from 13GByte by searching for common patterns, perhaps similar to the way bzip works.
Just a guess.
And, since it's so large, we probably can't do it by hand. So we would need to develop techniques to do it automatically. (Or semi-automatically.)
Of course, my "understanding" may be completely wrong.