But machine-oriented ATP is based on a symbolic-representation of formulas and terms. And the output is a proof formulated in the underlying logical calculus not just yes or no.
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.