But I have the impression Gowers dismisses the insights of what he calls machine-oriented ATP. These systems were --- perhaps are --- optimized on all levels of abstraction. From advances in the theory of which parts of the search space could be eliminated without loss of generality to optimizing the layout of c structs to improve cache locality.
But he's a mathematician, not an AI researcher - they have different goals.
Many AI researchers are interested in creating tools that solve problems (or proofs in this case).
Most mathematicians find proofs interesting for the insights they provide, not just the solution output.
You could say Gowers is looking for meta-proofs that provide insights on proof generation. It makes sense for him to emphasise the symbolic logic approach of GOFAI, here.
I would speculate Gowers is looking at higher-level abstractions that capture the essential semantics mathematicians are interested in - very much like a higher level programming language that humans understand.