> And vice versa. For it to do so, it has to be better than the human, also have a model of how the human thinks, and then be able to break down thinking it arrived at one way to something that makes sense to the human.

This is more or less what Gowers is after. And that's exactly why he wants GOFAI instead of ML. He wants to understand how "doing mathematics" works?