Exactly - machine-formulated ATP often ends up like machine-code, very similar to the proofs of Russell's Principia Mathematica. Extremely low-level formalisms great for procedural reasoning, but poor for human understanding.

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.