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 sh

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.