I like this analogy! I think it relates to what he was saying in the video about theorems now being 'data points' that you observe and build into wider theories. The change is that now the theorem proving itself, which used to require deep understanding, can now be done very quickly. There are lots of parallels to when genAI for image generation came out, artists were frustrated their work is seen as just an end result - AI obliterates the elegance and the process.

I am not a mathematician, but I imagine it will provide a huge landscape of possibilities to explore, and be a very different field. Almost like an observational science with links to all kinds of other disciplines. Maybe it reduces the satisfaction from proofs, but people climb mountains that other people have climbed, because they learn a lot on the way.