alt Hacker NewsFar outside my expertise, but it feels like the shaky assumption here is that the understanding and proof need to come in a specific order to be valuable. Can't we get all the meaty goodness by simplifying and generalizing the proofs now we know they exist? Sure, some insights will live in the discovery itself, and I guess it's nice to be the person who got to a proof first, but the real work (according to the mathematicians, afaict) is in the understanding and processing. In this way, it feels like it's moving towards being like most other science: mostly understanding things that are already there.
> 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.