I have not heard of Gowers, but I have heard of Gödel, Turing, and Church. In fact, Gödel showed for any non-trivial axiomatic system there are true statements which cannot be proved in the system. So there is that.
Well, none of those have worked on automated theorem proving. So there is that.
As for logic, I am sure Gowers knows about Gödel, Church and Turing, so that should not be a problem ...
Furthermore, your statement of Gödel's incompleteness result is wrong, as it directly contradicts Gödel's completeness result. It's not that you cannot prove all true statements for a non-trivial axiomatic formal system. But it is rather that your non-trivial axiomatic formal system does not mean what you might want it to mean as you will always have non-standard models alongside your intended standard model. So that's actually an argument FOR Gowers' approach, because it means that an automated mathematician needs to reach beyond formal logic and capture this elusive notion of intuition.
