I agree he seems quite disinterested in 'machine-oriented ATP'.

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.