> Can't we get all the meaty goodness by simplifying and generalizing the proofs now we know they exist?

Perhaps, but there is a danger: it is difficult to un-see things. At least for now, AI-generated proofs are likely to be of a somewhat brute-force nature. As each such proof pops into existence, two things happen: (1) it is much harder to maintain an untainted mind and go on to discover alternative, perhaps deeper and more conceptual, proofs that cannot be obtained by massaging and cleaning up a more brute-force approach (think of this as getting 'stuck in a local minimum', if you like), and (2) at a societal level there is thereafter much less incentive to attempt to do so (announcing a proof of a previous unproven result is, for now, far more prestigious than announcing a much better, more elegant, proof of a known result).

One could ask why we prefer conceptual explanations to brute-force proofs; after all, a proof is a proof, isn't it? I suppose one reasonable answer is that conceptual explanations lead more readily to new questions and that there's also intrinsic beauty in such explanations -- though, of course, many outside the field will simply not care.