I agree. I am just reading through Gowers paper on automatic theorem proving. I think once the machines are capable of automatic definitions (according to some

I agree. I am just reading through Gowers paper on automatic theorem proving. I think once the machines are capable of automatic definitions (according to some definition of beautiful which limits to what humans consider beautiful, for example one based on entropy), all the bets are off. Humans will then struggle to understand the concepts involved with their limited brains.