I'm not sure that elegance will be so easy to train for, the same way that writing skill has plateaued (or arguably declined) since earlier models. "Have you solved the problem" is verifiable, but questions of taste are harder to pin down.

You can select for 'short proof', or 'elementary proof', or assign the 'cost' of the proof as a some combination of its length, the number and complexity of the new terms it needs to define, and so on.

This might not help you with finding the proof, but once you have a machine that can produce several different proofs, you can select among them and incrementally polish the best one.

I think this is the 'easier' part.

This sounds kind of like unreadable code, though. So it's more than just taste.